Theorem 3mix2d 1354

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

Syntax hints:   → wi 4   ∨ w3o 1100

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 210  df-or 861  df-3or 1102

This theorem is referenced by:  sosn  5746  f1dom3fv3dif  7264  f1dom3el3dif  7265  xpord3inddlem  8146  elfiun  9386  fpwwe2lem12  10623  fvf1tp  13818  swrdnd0  14691  lcmfunsnlem2lem2  16693  dyaddisjlem  25719  ltssolem1  27801  tgcolg  28785  btwncolg2  28787  hlln  28838  btwnlng2  28851  elplngid  29018  hpgssplng  29032  frgrregorufr0  30612  constrsslem  34072  constrlccllem  34084  colineartriv2  36455  gpgprismgriedgdmss  48701  gpgvtxedg0  48712  gpgvtxedg1  48713  gpgedgiov  48714  eenglngeehlnmlem2  49398