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 ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃))

Syntax hints:   → wi 4   ∨ w3o 1102

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 210  df-or 861  df-3or 1104

This theorem is referenced by:  sosn  5748  f1dom3fv3dif  7266  f1dom3el3dif  7267  xpord3inddlem  8146  elfiun  9386  fpwwe2lem12  10622  fvf1tp  13818  swrdnd0  14691  lcmfunsnlem2lem2  16692  dyaddisjlem  25754  ltssolem1  27839  tgcolg  28823  btwncolg2  28825  hlln  28879  btwnlng2  28893  elplngid  29064  hpgssplng  29078  frgrregorufr0  30675  constrsslem  34131  constrlccllem  34143  colineartriv2  36560  gpgprismgriedgdmss  48817  gpgvtxedg0  48828  gpgvtxedg1  48829  gpgedgiov  48830  eenglngeehlnmlem2  49518