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

Theorem 3orim123d 1446
Description: Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997.)
Hypotheses
Ref Expression
3anim123d.1 (𝜑 → (𝜓𝜒))
3anim123d.2 (𝜑 → (𝜃𝜏))
3anim123d.3 (𝜑 → (𝜂𝜁))
Assertion
Ref Expression
3orim123d (𝜑 → ((𝜓𝜃𝜂) → (𝜒𝜏𝜁)))

Proof of Theorem 3orim123d
StepHypRef Expression
1 3anim123d.1 . . . 4 (𝜑 → (𝜓𝜒))
2 3anim123d.2 . . . 4 (𝜑 → (𝜃𝜏))
31, 2orim12d 967 . . 3 (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
4 3anim123d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4orim12d 967 . 2 (𝜑 → (((𝜓𝜃) ∨ 𝜂) → ((𝜒𝜏) ∨ 𝜁)))
6 df-3or 1088 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
7 df-3or 1088 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∨ 𝜁))
85, 6, 73imtr4g 296 1 (𝜑 → ((𝜓𝜃𝜂) → (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 848  w3o 1086
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-an 396  df-or 849  df-3or 1088
This theorem is referenced by:  fr3nr  7792  soxp  8154  poxp3  8175  zorn2lem6  10541  fpwwe2lem11  10681  fpwwe2lem12  10682  sltres  27707  colinearalglem4  28924  chnso  33004  constrconj  33786  colinearxfr  36076  weiunso  36467  fin2so  37614  frege133d  43778  el1fzopredsuc  47337  fmtno4prmfac  47559
  Copyright terms: Public domain W3C validator