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

Theorem 3orbi123d 1437
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 919 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4orbi12d 919 . 2 (𝜑 → (((𝜓𝜃) ∨ 𝜂) ↔ ((𝜒𝜏) ∨ 𝜁)))
6 df-3or 1088 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
7 df-3or 1088 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∨ 𝜁))
85, 6, 73bitr4g 314 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wo 848  w3o 1086
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 207  df-or 849  df-3or 1088
This theorem is referenced by:  moeq3  3718  soeq1  5613  solin  5619  soinxp  5767  ordtri3or  6416  isosolem  7367  sorpssi  7749  dfwe2  7794  f1oweALT  7997  soxp  8154  frxp3  8176  xpord3inddlem  8179  elfiun  9470  sornom  10317  ltsopr  11072  elz  12615  dyaddisj  25631  istrkgl  28466  istrkgld  28467  axtgupdim2  28479  tgdim01  28515  tglngval  28559  tgellng  28561  colcom  28566  colrot1  28567  legso  28607  lncom  28630  lnrot1  28631  lnrot2  28632  ttgval  28883  ttgvalOLD  28884  colinearalg  28925  axlowdim2  28975  axlowdim  28976  elntg  28999  elntg2  29000  nb3grprlem2  29398  frgrwopreg  30342  constrsuc  33779  istrkg2d  34681  axtgupdim2ALTV  34683  brcolinear2  36059  colineardim1  36062  colinearperm1  36063  fin2so  37614  uneqsn  44038  3orbi123  44531  gpgov  48001  gpgedgel  48007  gpgedgvtx0  48019  gpgedgvtx1  48020  gpg3kgrtriexlem6  48044
  Copyright terms: Public domain W3C validator