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  9325  fpwwe2lem12  10544  fvf1tp  13700  swrdnd0  14572  lcmfunsnlem2lem2  16557  dyaddisjlem  25543  sltsolem1  27634  tgcolg  28552  btwncolg2  28554  hlln  28605  btwnlng2  28618  frgrregorufr0  30325  constrsslem  33826  constrlccllem  33838  colineartriv2  36184  gpgprismgriedgdmss  48214  gpgvtxedg0  48225  gpgvtxedg1  48226  gpgedgiov  48227  eenglngeehlnmlem2  48900