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

Theorem 3orbi123i 1188
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 929 . . 3 ((𝜑𝜒) ↔ (𝜓𝜃))
4 bi3.3 . . 3 (𝜏𝜂)
53, 4orbi12i 929 . 2 (((𝜑𝜒) ∨ 𝜏) ↔ ((𝜓𝜃) ∨ 𝜂))
6 df-3or 1101 . 2 ((𝜑𝜒𝜏) ↔ ((𝜑𝜒) ∨ 𝜏))
7 df-3or 1101 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
85, 6, 73bitr4i 294 1 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wo 865  w3o 1099
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 198  df-or 866  df-3or 1101
This theorem is referenced by:  ne3anior  3082  wecmpep  5314  cnvso  5899  sorpss  7179  ordon  7219  soxp  7531  dford2  8771  elfz0lmr  12814  axlowdimlem6  26051  elxrge02  29975  brtp  31970  dfon2  32026  sltsolem1  32156  frege129d  38560  dfxlim2  40559
  Copyright terms: Public domain W3C validator