Theorem 3mix3d 1357

Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)

Hypothesis

Ref	Expression
3mixd.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
3mix3d	⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓))

Proof of Theorem 3mix3d

Step	Hyp	Ref	Expression
1		3mixd.1	. 2 ⊢ (𝜑 → 𝜓)
2		3mix3 1351	. 2 ⊢ (𝜓 → (𝜒 ∨ 𝜃 ∨ 𝜓))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ w3o 1102

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 1104

This theorem is referenced by:  xpord3inddlem  8146  elfiun  9386  nnnegz  12589  fvf1tp  13818  hashv01gt1  14377  lcmfunsnlem2lem2  16692  cshwshashlem1  17150  dyaddisjlem  25754  zabsle1  27460  noextendgt  27834  ltssolem1  27839  nodense  27856  btwncolg3  28826  btwnlng3  28894  frgr3vlem2  30625  3vfriswmgr  30629  frgrregorufr0  30675  constrcccllem  34144  weiunso  36977  fnwe2lem3  43779  omcl2  44060  gpgprismgriedgdmss  48817  gpgedgvtx1  48827  gpgvtxedg0  48828  gpgvtxedg1  48829  gpg3kgrtriexlem6  48853  gpgprismgr4cycllem3  48862  eenglngeehlnmlem2  49518