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  5711  f1dom3fv3dif  7216  f1dom3el3dif  7217  xpord3inddlem  8097  elfiun  9336  fpwwe2lem12  10556  fvf1tp  13739  swrdnd0  14611  lcmfunsnlem2lem2  16599  dyaddisjlem  25572  ltssolem1  27653  tgcolg  28636  btwncolg2  28638  hlln  28689  btwnlng2  28702  frgrregorufr0  30409  constrsslem  33901  constrlccllem  33913  colineartriv2  36266  gpgprismgriedgdmss  48540  gpgvtxedg0  48551  gpgvtxedg1  48552  gpgedgiov  48553  eenglngeehlnmlem2  49226