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  5708  f1dom3fv3dif  7211  f1dom3el3dif  7212  xpord3inddlem  8093  elfiun  9324  fpwwe2lem12  10543  fvf1tp  13703  swrdnd0  14575  lcmfunsnlem2lem2  16560  dyaddisjlem  25533  sltsolem1  27624  tgcolg  28542  btwncolg2  28544  hlln  28595  btwnlng2  28608  frgrregorufr0  30315  constrsslem  33765  constrlccllem  33777  colineartriv2  36123  gpgprismgriedgdmss  48166  gpgvtxedg0  48177  gpgvtxedg1  48178  gpgedgiov  48179  eenglngeehlnmlem2  48853