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  8152  xpord3inddlem  8175  elfiun  9427  nnnegz  12701  fvf1tp  13934  hashv01gt1  14494  lcmfunsnlem2lem2  16821  cshwshashlem1  17280  dyaddisjlem  25923  zabsle1  27630  noextendgt  28034  ltssolem1  28039  nodense  28056  btwncolg3  29027  btwnlng3  29096  frgr3vlem2  30882  3vfriswmgr  30886  frgrregorufr0  30932  constrcccllem  34434  weiunso  37348  omcl2  44442  gpgprismgriedgdmss  49257  gpgedgvtx1  49267  gpgvtxedg0  49268  gpgvtxedg1  49269  gpg3kgrtriexlem6  49293  gpgprismgr4cycllem3  49302  eenglngeehlnmlem2  49958