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

Theorem 3orbi123d 1395
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 745 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4orbi12d 745 . 2 (𝜑 → (((𝜓𝜃) ∨ 𝜂) ↔ ((𝜒𝜏) ∨ 𝜁)))
6 df-3or 1037 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
7 df-3or 1037 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∨ 𝜁))
85, 6, 73bitr4g 303 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  w3o 1035
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 385  df-3or 1037
This theorem is referenced by:  moeq3  3370  soeq1  5024  solin  5028  soinxp  5154  ordtri3or  5724  isosolem  6562  sorpssi  6908  dfwe2  6943  f1oweALT  7112  soxp  7250  elfiun  8296  sornom  9059  ltsopr  9814  elz  11339  dyaddisj  23304  istrkgl  25291  istrkgld  25292  axtgupdim2  25304  tgdim01  25336  tglngval  25380  tgellng  25382  colcom  25387  colrot1  25388  legso  25428  lncom  25451  lnrot1  25452  lnrot2  25453  ttgval  25689  colinearalg  25724  axlowdim2  25774  axlowdim  25775  elntg  25798  nb3grprlem2  26204  frgrregorufr0  27081  istrkg2d  30504  axtgupdim2OLD  30506  brcolinear2  31860  colineardim1  31863  colinearperm1  31864  fin2so  33067  uneqsn  37842  3orbi123  38238
  Copyright terms: Public domain W3C validator