Theorem 3orim123d 1473

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 979	. . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
4		3anim123d.3	. . 3 ⊢ (𝜑 → (𝜂 → 𝜁))
5	3, 4	orim12d 979	. 2 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∨ 𝜂) → ((𝜒 ∨ 𝜏) ∨ 𝜁)))
6		df-3or 1104	. 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))
7		df-3or 1104	. 2 ⊢ ((𝜒 ∨ 𝜏 ∨ 𝜁) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁))
8	5, 6, 7	3imtr4g 299	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) → (𝜒 ∨ 𝜏 ∨ 𝜁)))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104

This theorem is used by:  3orim123da  1474  fr3nr  7818  soxp  8178  poxp3  8204  zorn2lem6  10618  fpwwe2lem11  10765  fpwwe2lem12  10766  chnso  18848  ltsres  28076  colinearalglem4  29544  constrconj  34488  vonf1wev  36077  vonf1owevOLD  36079  colinearxfr  37055  weiunso  37469  fin2so  38798  frege133d  45026  chnerlem3  48167  el1fzopredsuc  48669  fmtno4prmfac  48930