Theorem 3orim123d 1447

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

Step	Hyp	Ref	Expression
1		3anim123d.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2		3anim123d.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜏))
3	1, 2	orim12d 967	. . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
4		3anim123d.3	. . 3 ⊢ (𝜑 → (𝜂 → 𝜁))
5	3, 4	orim12d 967	. 2 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∨ 𝜂) → ((𝜒 ∨ 𝜏) ∨ 𝜁)))
6		df-3or 1088	. 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))
7		df-3or 1088	. 2 ⊢ ((𝜒 ∨ 𝜏 ∨ 𝜁) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁))
8	5, 6, 7	3imtr4g 296	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) → (𝜒 ∨ 𝜏 ∨ 𝜁)))

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  7726  soxp  8079  poxp3  8100  zorn2lem6  10423  fpwwe2lem11  10564  fpwwe2lem12  10565  chnso  18590  ltsres  27626  colinearalglem4  28978  constrconj  33889  vonf1owev  35290  colinearxfr  36257  weiunso  36648  fin2so  37928  frege133d  44192  chnerlem3  47314  el1fzopredsuc  47774  fmtno4prmfac  48035