Theorem 3mix2d 1338

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

Syntax hints:   → wi 4   ∨ w3o 1085

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 848  df-3or 1087

This theorem is referenced by:  sosn  5725  f1dom3fv3dif  7243  f1dom3el3dif  7244  xpord3inddlem  8133  elfiun  9381  fpwwe2lem12  10595  fvf1tp  13751  swrdnd0  14622  lcmfunsnlem2lem2  16609  dyaddisjlem  25496  sltsolem1  27587  tgcolg  28481  btwncolg2  28483  hlln  28534  btwnlng2  28547  frgrregorufr0  30253  constrsslem  33731  constrlccllem  33743  colineartriv2  36056  gpgprismgriedgdmss  48043  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgedgiov  48056  eenglngeehlnmlem2  48727