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  5711  f1dom3fv3dif  7214  f1dom3el3dif  7215  xpord3inddlem  8096  elfiun  9333  fpwwe2lem12  10553  fvf1tp  13709  swrdnd0  14581  lcmfunsnlem2lem2  16566  dyaddisjlem  25552  ltssolem1  27643  tgcolg  28626  btwncolg2  28628  hlln  28679  btwnlng2  28692  frgrregorufr0  30399  constrsslem  33898  constrlccllem  33910  colineartriv2  36262  gpgprismgriedgdmss  48298  gpgvtxedg0  48309  gpgvtxedg1  48310  gpgedgiov  48311  eenglngeehlnmlem2  48984