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  5742  f1dom3fv3dif  7265  f1dom3el3dif  7266  xpord3inddlem  8152  elfiun  9400  fpwwe2lem12  10651  fvf1tp  13850  swrdnd0  14727  lcmfunsnlem2lem2  16729  dyaddisjlem  25823  ltssolem1  27911  tgcolg  28896  btwncolg2  28898  hlln  28952  btwnlng2  28967  elplngid  29139  hpgssplng  29153  frgrregorufr0  30804  constrsslem  34251  constrlccllem  34263  colineartriv2  36648  gpgprismgriedgdmss  48968  gpgvtxedg0  48979  gpgvtxedg1  48980  gpgedgiov  48981  eenglngeehlnmlem2  49668