Theorem 3mix2d 1356

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  sosn  5746  f1dom3fv3dif  7268  f1dom3el3dif  7269  xpord3inddlem  8155  elfiun  9403  fpwwe2lem12  10654  fvf1tp  13852  swrdnd0  14729  lcmfunsnlem2lem2  16733  dyaddisjlem  25824  ltssolem1  27909  tgcolg  28894  btwncolg2  28896  hlln  28950  btwnlng2  28965  elplngid  29137  hpgssplng  29151  frgrregorufr0  30790  constrsslem  34238  constrlccllem  34250  colineartriv2  36635  gpgprismgriedgdmss  48955  gpgvtxedg0  48966  gpgvtxedg1  48967  gpgedgiov  48968  eenglngeehlnmlem2  49655