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

Theorem 3orbi123d 1390
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 742 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4orbi12d 742 . 2 (𝜑 → (((𝜓𝜃) ∨ 𝜂) ↔ ((𝜒𝜏) ∨ 𝜁)))
6 df-3or 1032 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
7 df-3or 1032 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∨ 𝜁))
85, 6, 73bitr4g 302 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wo 382  w3o 1030
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 196  df-or 384  df-3or 1032
This theorem is referenced by:  moeq3  3350  soeq1  4978  solin  4982  soinxp  5106  ordtri3or  5672  isosolem  6497  sorpssi  6841  dfwe2  6873  f1oweALT  7043  soxp  7177  elfiun  8219  sornom  8982  ltsopr  9733  elz  11256  dyaddisj  23170  istrkgl  25157  istrkgld  25158  axtgupdim2  25170  tgdim01  25202  tglngval  25246  tgellng  25248  colcom  25253  colrot1  25254  legso  25294  lncom  25317  lnrot1  25318  lnrot2  25319  ttgval  25555  colinearalg  25590  axlowdim2  25640  axlowdim  25641  elntg  25664  nb3graprlem2  25981  frgraregorufr0  26579  istrkg2d  29997  axtgupdim2OLD  29999  brcolinear2  31335  colineardim1  31338  colinearperm1  31339  fin2so  32566  uneqsn  37341  3orbi123  37738  nb3grprlem2  40609  frgrregorufr0  41489
  Copyright terms: Public domain W3C validator