Theorem 3mix2d 1356

Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)

Hypothesis

Ref	Expression
3mixd.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
3mix2d	⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃))

Proof of Theorem 3mix2d

Step	Hyp	Ref	Expression
1		3mixd.1	. 2 ⊢ (𝜑 → 𝜓)
2		3mix2 1350	. 2 ⊢ (𝜓 → (𝜒 ∨ 𝜓 ∨ 𝜃))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃))

This proof depends on syntax axioms:   → wi 4   ∨ 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-or 862  df-3or 1104

This theorem is used by:  sosn  5738  f1dom3fv3dif  7270  f1dom3el3dif  7271  xpord3inddlem  8164  elfiun  9415  fpwwe2lem12  10720  fvf1tp  13922  swrdnd0  14800  lcmfunsnlem2lem2  16807  dyaddisjlem  25909  ltssolem1  28025  tgcolg  29010  btwncolg2  29012  hlln  29066  btwnlng2  29081  elplngid  29253  hpgssplng  29267  frgrregorufr0  30918  constrsslem  34366  constrlccllem  34378  colineartriv2  36813  gpgprismgriedgdmss  49119  gpgvtxedg0  49130  gpgvtxedg1  49131  gpgedgiov  49132  eenglngeehlnmlem2  49819