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  8148  xpord3inddlem  8171  elfiun  9423  nnnegz  12697  fvf1tp  13930  hashv01gt1  14490  lcmfunsnlem2lem2  16815  cshwshashlem1  17274  dyaddisjlem  25917  zabsle1  27624  noextendgt  28028  ltssolem1  28033  nodense  28050  btwncolg3  29021  btwnlng3  29090  frgr3vlem2  30876  3vfriswmgr  30880  frgrregorufr0  30926  constrcccllem  34429  weiunso  37329  omcl2  44411  gpgprismgriedgdmss  49226  gpgedgvtx1  49236  gpgvtxedg0  49237  gpgvtxedg1  49238  gpg3kgrtriexlem6  49262  gpgprismgr4cycllem3  49271  eenglngeehlnmlem2  49926