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

Theorem 3orbi123d 1426
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 912 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4orbi12d 912 . 2 (𝜑 → (((𝜓𝜃) ∨ 𝜂) ↔ ((𝜒𝜏) ∨ 𝜁)))
6 df-3or 1080 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
7 df-3or 1080 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∨ 𝜁))
85, 6, 73bitr4g 315 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wo 841  w3o 1078
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 208  df-or 842  df-3or 1080
This theorem is referenced by:  moeq3  3700  soeq1  5487  solin  5491  soinxp  5626  ordtri3or  6216  isosolem  7089  sorpssi  7444  dfwe2  7485  f1oweALT  7662  soxp  7812  elfiun  8882  sornom  9687  ltsopr  10442  elz  11971  dyaddisj  24124  istrkgl  26171  istrkgld  26172  axtgupdim2  26184  tgdim01  26220  tglngval  26264  tgellng  26266  colcom  26271  colrot1  26272  legso  26312  lncom  26335  lnrot1  26336  lnrot2  26337  ttgval  26588  colinearalg  26623  axlowdim2  26673  axlowdim  26674  elntg  26697  elntg2  26698  nb3grprlem2  27090  frgrwopreg  28029  istrkg2d  31836  axtgupdim2ALTV  31838  brcolinear2  33416  colineardim1  33419  colinearperm1  33420  fin2so  34760  uneqsn  40251  3orbi123  40722
  Copyright terms: Public domain W3C validator