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

Theorem 3orbi123i 1244
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 541 . . 3 ((𝜑𝜒) ↔ (𝜓𝜃))
4 bi3.3 . . 3 (𝜏𝜂)
53, 4orbi12i 541 . 2 (((𝜑𝜒) ∨ 𝜏) ↔ ((𝜓𝜃) ∨ 𝜂))
6 df-3or 1031 . 2 ((𝜑𝜒𝜏) ↔ ((𝜑𝜒) ∨ 𝜏))
7 df-3or 1031 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
85, 6, 73bitr4i 290 1 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wo 381  w3o 1029
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 195  df-or 383  df-3or 1031
This theorem is referenced by:  ne3anior  2874  wecmpep  5019  cnvso  5576  sorpss  6817  ordon  6851  soxp  7154  dford2  8377  axlowdimlem6  25572  elxrge02  28764  brtp  30685  socnv  30701  dfon2  30734  sltsolem1  30860  frege129d  36857  elfz0lmr  40173
  Copyright terms: Public domain W3C validator