Theorem 3mix2d 1344

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

Syntax hints:   → wi 4   ∨ w3o 1091

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 208  df-or 854  df-3or 1093

This theorem is referenced by:  sosn  5705  f1dom3fv3dif  7212  f1dom3el3dif  7213  xpord3inddlem  8094  elfiun  9333  fpwwe2lem12  10556  fvf1tp  13739  swrdnd0  14611  lcmfunsnlem2lem2  16599  dyaddisjlem  25580  ltssolem1  27657  tgcolg  28640  btwncolg2  28642  hlln  28693  btwnlng2  28706  frgrregorufr0  30412  constrsslem  33925  constrlccllem  33937  colineartriv2  36296  gpgprismgriedgdmss  48543  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgedgiov  48556  eenglngeehlnmlem2  49229