Theorem 3mix2d 1339

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 1333	. 2 ⊢ (𝜓 → (𝜒 ∨ 𝜓 ∨ 𝜃))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃))

Syntax hints:   → wi 4   ∨ 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-or 849  df-3or 1088

This theorem is referenced by:  sosn  5718  f1dom3fv3dif  7223  f1dom3el3dif  7224  xpord3inddlem  8104  elfiun  9343  fpwwe2lem12  10565  fvf1tp  13748  swrdnd0  14620  lcmfunsnlem2lem2  16608  dyaddisjlem  25562  ltssolem1  27639  tgcolg  28622  btwncolg2  28624  hlln  28675  btwnlng2  28688  frgrregorufr0  30394  constrsslem  33885  constrlccllem  33897  colineartriv2  36250  gpgprismgriedgdmss  48528  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgedgiov  48541  eenglngeehlnmlem2  49214