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

Theorem 3orbi123i 1153
 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 912 . . 3 ((𝜑𝜒) ↔ (𝜓𝜃))
4 bi3.3 . . 3 (𝜏𝜂)
53, 4orbi12i 912 . 2 (((𝜑𝜒) ∨ 𝜏) ↔ ((𝜓𝜃) ∨ 𝜂))
6 df-3or 1085 . 2 ((𝜑𝜒𝜏) ↔ ((𝜑𝜒) ∨ 𝜏))
7 df-3or 1085 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
85, 6, 73bitr4i 306 1 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∨ wo 844   ∨ 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 210  df-or 845  df-3or 1085 This theorem is referenced by:  ne3anior  3044  wecmpep  5520  cnvso  6122  sorpss  7458  epweon  7502  soxp  7834  dford2  9129  elfz0lmr  13214  axlowdimlem6  26853  elxrge02  30742  brtp  33244  dfon2  33296  poxp3  33363  sltsolem1  33475  frege129d  40872  dfxlim2  42891
 Copyright terms: Public domain W3C validator