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

Theorem 3orbi123d 1431
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 915 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4orbi12d 915 . 2 (𝜑 → (((𝜓𝜃) ∨ 𝜂) ↔ ((𝜒𝜏) ∨ 𝜁)))
6 df-3or 1084 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
7 df-3or 1084 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∨ 𝜁))
85, 6, 73bitr4g 316 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wo 843  w3o 1082
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 209  df-or 844  df-3or 1084
This theorem is referenced by:  moeq3  3705  soeq1  5496  solin  5500  soinxp  5635  ordtri3or  6225  isosolem  7102  sorpssi  7457  dfwe2  7498  f1oweALT  7675  soxp  7825  elfiun  8896  sornom  9701  ltsopr  10456  elz  11986  dyaddisj  24199  istrkgl  26246  istrkgld  26247  axtgupdim2  26259  tgdim01  26295  tglngval  26339  tgellng  26341  colcom  26346  colrot1  26347  legso  26387  lncom  26410  lnrot1  26411  lnrot2  26412  ttgval  26663  colinearalg  26698  axlowdim2  26748  axlowdim  26749  elntg  26772  elntg2  26773  nb3grprlem2  27165  frgrwopreg  28104  istrkg2d  31939  axtgupdim2ALTV  31941  brcolinear2  33521  colineardim1  33524  colinearperm1  33525  fin2so  34881  uneqsn  40380  3orbi123  40852
  Copyright terms: Public domain W3C validator