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  7303  f1dom3el3dif  7304  xpord3inddlem  8208  elfiun  9459  fpwwe2lem12  10766  fvf1tp  13969  swrdnd0  14849  lcmfunsnlem2lem2  16858  dyaddisjlem  25971  ltssolem1  28089  tgcolg  29074  btwncolg2  29076  hlln  29130  btwnlng2  29145  elplngid  29317  hpgssplng  29331  frgrregorufr0  30982  constrsslem  34484  constrlccllem  34496  colineartriv2  37048  gpgprismgriedgdmss  49423  gpgvtxedg0  49434  gpgvtxedg1  49435  gpgedgiov  49436  eenglngeehlnmlem2  50182