MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3orbi123d Structured version   Visualization version   GIF version

Theorem 3orbi123d 1438
Description: Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.)
Hypotheses
Ref Expression
bi3d.1 (𝜑 → (𝜓𝜒))
bi3d.2 (𝜑 → (𝜃𝜏))
bi3d.3 (𝜑 → (𝜂𝜁))
Assertion
Ref Expression
3orbi123d (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))

Proof of Theorem 3orbi123d
StepHypRef Expression
1 bi3d.1 . . . 4 (𝜑 → (𝜓𝜒))
2 bi3d.2 . . . 4 (𝜑 → (𝜃𝜏))
31, 2orbi12d 746 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4orbi12d 746 . 2 (𝜑 → (((𝜓𝜃) ∨ 𝜂) ↔ ((𝜒𝜏) ∨ 𝜁)))
6 df-3or 1055 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
7 df-3or 1055 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∨ 𝜁))
85, 6, 73bitr4g 303 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  w3o 1053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-or 384  df-3or 1055
This theorem is referenced by:  moeq3  3416  soeq1  5083  solin  5087  soinxp  5217  ordtri3or  5793  isosolem  6637  sorpssi  6985  dfwe2  7023  f1oweALT  7194  soxp  7335  elfiun  8377  sornom  9137  ltsopr  9892  elz  11417  dyaddisj  23410  istrkgl  25402  istrkgld  25403  axtgupdim2  25415  tgdim01  25447  tglngval  25491  tgellng  25493  colcom  25498  colrot1  25499  legso  25539  lncom  25562  lnrot1  25563  lnrot2  25564  ttgval  25800  colinearalg  25835  axlowdim2  25885  axlowdim  25886  elntg  25909  nb3grprlem2  26327  frgrwopreg  27303  istrkg2d  30872  axtgupdim2OLD  30874  brcolinear2  32290  colineardim1  32293  colinearperm1  32294  fin2so  33526  uneqsn  38638  3orbi123  39034
  Copyright terms: Public domain W3C validator