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

Theorem 3orbi123d 1563
 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 947 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4orbi12d 947 . 2 (𝜑 → (((𝜓𝜃) ∨ 𝜂) ↔ ((𝜒𝜏) ∨ 𝜁)))
6 df-3or 1112 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
7 df-3or 1112 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∨ 𝜁))
85, 6, 73bitr4g 306 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∨ wo 878   ∨ w3o 1110 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 199  df-or 879  df-3or 1112 This theorem is referenced by:  moeq3  3608  soeq1  5285  solin  5289  soinxp  5422  ordtri3or  5999  isosolem  6857  sorpssi  7208  dfwe2  7247  f1oweALT  7417  soxp  7559  elfiun  8611  sornom  9421  ltsopr  10176  elz  11713  dyaddisj  23769  istrkgl  25777  istrkgld  25778  axtgupdim2  25790  tgdim01  25826  tglngval  25870  tgellng  25872  colcom  25877  colrot1  25878  legso  25918  lncom  25941  lnrot1  25942  lnrot2  25943  ttgval  26181  colinearalg  26216  axlowdim2  26266  axlowdim  26267  elntg  26290  elntg2  26291  nb3grprlem2  26686  frgrwopreg  27700  istrkg2d  31289  axtgupdim2OLD  31291  brcolinear2  32699  colineardim1  32702  colinearperm1  32703  fin2so  33934  uneqsn  39156  3orbi123  39550
 Copyright terms: Public domain W3C validator