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  8104  elfiun  9343  nnnegz  12527  fvf1tp  13748  hashv01gt1  14307  lcmfunsnlem2lem2  16608  cshwshashlem1  17066  dyaddisjlem  25562  zabsle1  27259  noextendgt  27634  ltssolem1  27639  nodense  27656  btwncolg3  28625  btwnlng3  28689  frgr3vlem2  30344  3vfriswmgr  30348  frgrregorufr0  30394  constrcccllem  33898  weiunso  36648  fnwe2lem3  43480  omcl2  43761  gpgprismgriedgdmss  48528  gpgedgvtx1  48538  gpgvtxedg0  48539  gpgvtxedg1  48540  gpg3kgrtriexlem6  48564  gpgprismgr4cycllem3  48573  eenglngeehlnmlem2  49214