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  5737  f1dom3fv3dif  7273  f1dom3el3dif  7274  xpord3inddlem  8174  elfiun  9426  fpwwe2lem12  10731  fvf1tp  13933  swrdnd0  14812  lcmfunsnlem2lem2  16820  dyaddisjlem  25922  ltssolem1  28038  tgcolg  29023  btwncolg2  29025  hlln  29079  btwnlng2  29094  elplngid  29266  hpgssplng  29280  frgrregorufr0  30931  constrsslem  34420  constrlccllem  34432  colineartriv2  36926  gpgprismgriedgdmss  49244  gpgvtxedg0  49255  gpgvtxedg1  49256  gpgedgiov  49257  eenglngeehlnmlem2  49945