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  5719  f1dom3fv3dif  7224  f1dom3el3dif  7225  xpord3inddlem  8106  elfiun  9345  fpwwe2lem12  10565  fvf1tp  13721  swrdnd0  14593  lcmfunsnlem2lem2  16578  dyaddisjlem  25564  ltssolem1  27655  tgcolg  28638  btwncolg2  28640  hlln  28691  btwnlng2  28704  frgrregorufr0  30411  constrsslem  33919  constrlccllem  33931  colineartriv2  36284  gpgprismgriedgdmss  48412  gpgvtxedg0  48423  gpgvtxedg1  48424  gpgedgiov  48425  eenglngeehlnmlem2  49098