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

Theorem 3orbi123i 1245
 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 542 . . 3 ((𝜑𝜒) ↔ (𝜓𝜃))
4 bi3.3 . . 3 (𝜏𝜂)
53, 4orbi12i 542 . 2 (((𝜑𝜒) ∨ 𝜏) ↔ ((𝜓𝜃) ∨ 𝜂))
6 df-3or 1032 . 2 ((𝜑𝜒𝜏) ↔ ((𝜑𝜒) ∨ 𝜏))
7 df-3or 1032 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
85, 6, 73bitr4i 291 1 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∨ wo 382   ∨ w3o 1030 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 196  df-or 384  df-3or 1032 This theorem is referenced by:  ne3anior  2875  wecmpep  5030  cnvso  5591  sorpss  6840  ordon  6874  soxp  7177  dford2  8400  axlowdimlem6  25627  elxrge02  28971  brtp  30892  socnv  30908  dfon2  30941  sltsolem1  31067  frege129d  37074  elfz0lmr  40367
 Copyright terms: Public domain W3C validator