Theorem 3mix3d 1340

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

Syntax hints:   → wi 4   ∨ w3o 1086

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 207  df-or 849  df-3or 1088

This theorem is referenced by:  xpord3inddlem  8106  elfiun  9345  nnnegz  12503  fvf1tp  13721  hashv01gt1  14280  lcmfunsnlem2lem2  16578  cshwshashlem1  17035  dyaddisjlem  25564  zabsle1  27275  noextendgt  27650  ltssolem1  27655  nodense  27672  btwncolg3  28641  btwnlng3  28705  frgr3vlem2  30361  3vfriswmgr  30365  frgrregorufr0  30411  constrcccllem  33932  weiunso  36682  fnwe2lem3  43409  omcl2  43690  gpgprismgriedgdmss  48412  gpgedgvtx1  48422  gpgvtxedg0  48423  gpgvtxedg1  48424  gpg3kgrtriexlem6  48448  gpgprismgr4cycllem3  48457  eenglngeehlnmlem2  49098