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  8097  elfiun  9336  nnnegz  12518  fvf1tp  13739  hashv01gt1  14298  lcmfunsnlem2lem2  16599  cshwshashlem1  17057  dyaddisjlem  25572  zabsle1  27273  noextendgt  27648  ltssolem1  27653  nodense  27670  btwncolg3  28639  btwnlng3  28703  frgr3vlem2  30359  3vfriswmgr  30363  frgrregorufr0  30409  constrcccllem  33914  weiunso  36664  fnwe2lem3  43498  omcl2  43779  gpgprismgriedgdmss  48540  gpgedgvtx1  48550  gpgvtxedg0  48551  gpgvtxedg1  48552  gpg3kgrtriexlem6  48576  gpgprismgr4cycllem3  48585  eenglngeehlnmlem2  49226