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

Theorem 3orbi123d 1432
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 916 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4orbi12d 916 . 2 (𝜑 → (((𝜓𝜃) ∨ 𝜂) ↔ ((𝜒𝜏) ∨ 𝜁)))
6 df-3or 1085 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
7 df-3or 1085 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∨ 𝜁))
85, 6, 73bitr4g 313 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wo 845  w3o 1083
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 206  df-or 846  df-3or 1085
This theorem is referenced by:  moeq3  3706  soeq1  5615  solin  5619  soinxp  5763  ordtri3or  6408  isosolem  7359  sorpssi  7740  dfwe2  7782  f1oweALT  7986  soxp  8143  frxp3  8165  xpord3inddlem  8168  elfiun  9473  sornom  10320  ltsopr  11075  elz  12612  dyaddisj  25616  istrkgl  28385  istrkgld  28386  axtgupdim2  28398  tgdim01  28434  tglngval  28478  tgellng  28480  colcom  28485  colrot1  28486  legso  28526  lncom  28549  lnrot1  28550  lnrot2  28551  ttgval  28802  ttgvalOLD  28803  colinearalg  28844  axlowdim2  28894  axlowdim  28895  elntg  28918  elntg2  28919  nb3grprlem2  29317  frgrwopreg  30256  constrsuc  33596  istrkg2d  34512  axtgupdim2ALTV  34514  brcolinear2  35882  colineardim1  35885  colinearperm1  35886  fin2so  37308  uneqsn  43692  3orbi123  44187
  Copyright terms: Public domain W3C validator