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 ⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  fnwe2lem4  8185  xpord3inddlem  8208  elfiun  9459  nnnegz  12736  fvf1tp  13969  hashv01gt1  14530  lcmfunsnlem2lem2  16858  cshwshashlem1  17317  dyaddisjlem  25971  zabsle1  27680  noextendgt  28084  ltssolem1  28089  nodense  28106  btwncolg3  29077  btwnlng3  29146  frgr3vlem2  30932  3vfriswmgr  30936  frgrregorufr0  30982  constrcccllem  34497  weiunso  37469  omcl2  44596  gpgprismgriedgdmss  49423  gpgedgvtx1  49433  gpgvtxedg0  49434  gpgvtxedg1  49435  gpg3kgrtriexlem6  49459  gpgprismgr4cycllem3  49468  eenglngeehlnmlem2  50182