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  8152  elfiun  9400  nnnegz  12618  fvf1tp  13850  hashv01gt1  14409  lcmfunsnlem2lem2  16729  cshwshashlem1  17187  dyaddisjlem  25823  zabsle1  27532  noextendgt  27906  ltssolem1  27911  nodense  27928  btwncolg3  28899  btwnlng3  28968  frgr3vlem2  30754  3vfriswmgr  30758  frgrregorufr0  30804  constrcccllem  34264  weiunso  37085  fnwe2lem3  43893  omcl2  44174  gpgprismgriedgdmss  48968  gpgedgvtx1  48978  gpgvtxedg0  48979  gpgvtxedg1  48980  gpg3kgrtriexlem6  49004  gpgprismgr4cycllem3  49013  eenglngeehlnmlem2  49668