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

Theorem 3orbi123i 1155
Description: Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)
Hypotheses
Ref Expression
bi3.1 (𝜑𝜓)
bi3.2 (𝜒𝜃)
bi3.3 (𝜏𝜂)
Assertion
Ref Expression
3orbi123i ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))

Proof of Theorem 3orbi123i
StepHypRef Expression
1 bi3.1 . . . 4 (𝜑𝜓)
2 bi3.2 . . . 4 (𝜒𝜃)
31, 2orbi12i 914 . . 3 ((𝜑𝜒) ↔ (𝜓𝜃))
4 bi3.3 . . 3 (𝜏𝜂)
53, 4orbi12i 914 . 2 (((𝜑𝜒) ∨ 𝜏) ↔ ((𝜓𝜃) ∨ 𝜂))
6 df-3or 1087 . 2 ((𝜑𝜒𝜏) ↔ ((𝜑𝜒) ∨ 𝜏))
7 df-3or 1087 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
85, 6, 73bitr4i 303 1 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wo 847  w3o 1085
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 207  df-or 848  df-3or 1087
This theorem is referenced by:  ne3anior  3034  otthne  5497  brtp  5533  wecmpep  5681  cnvso  6310  sorpss  7747  epweon  7794  epweonALT  7795  soxp  8153  dford2  9658  elfz0lmr  13818  hash3tpde  14529  sltsolem1  27735  axlowdimlem6  28977  elxrge02  32899  dfon2  35774  frege129d  43753  dfxlim2  45804  usgrexmpl2trifr  47932
  Copyright terms: Public domain W3C validator