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:  xpord3inddlem  8164  elfiun  9415  nnnegz  12689  fvf1tp  13922  hashv01gt1  14482  lcmfunsnlem2lem2  16807  cshwshashlem1  17266  dyaddisjlem  25909  zabsle1  27616  noextendgt  28020  ltssolem1  28025  nodense  28042  btwncolg3  29013  btwnlng3  29082  frgr3vlem2  30868  3vfriswmgr  30872  frgrregorufr0  30918  constrcccllem  34379  weiunso  37234  fnwe2lem3  44038  omcl2  44319  gpgprismgriedgdmss  49119  gpgedgvtx1  49129  gpgvtxedg0  49130  gpgvtxedg1  49131  gpg3kgrtriexlem6  49155  gpgprismgr4cycllem3  49164  eenglngeehlnmlem2  49819