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  5750  f1dom3fv3dif  7268  f1dom3el3dif  7269  xpord3inddlem  8152  elfiun  9393  fpwwe2lem12  10638  fvf1tp  13836  swrdnd0  14713  lcmfunsnlem2lem2  16715  dyaddisjlem  25785  ltssolem1  27870  tgcolg  28854  btwncolg2  28856  hlln  28910  btwnlng2  28924  elplngid  29095  hpgssplng  29109  frgrregorufr0  30722  constrsslem  34171  constrlccllem  34183  colineartriv2  36573  gpgprismgriedgdmss  48850  gpgvtxedg0  48861  gpgvtxedg1  48862  gpgedgiov  48863  eenglngeehlnmlem2  49551