Theorem 3mix3d 1339

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 1333	. 2 ⊢ (𝜓 → (𝜒 ∨ 𝜃 ∨ 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ w3o 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-or 848  df-3or 1087

This theorem is referenced by:  xpord3inddlem  8093  elfiun  9325  nnnegz  12482  fvf1tp  13700  hashv01gt1  14259  lcmfunsnlem2lem2  16557  cshwshashlem1  17014  dyaddisjlem  25543  zabsle1  27254  noextendgt  27629  sltsolem1  27634  nodense  27651  btwncolg3  28555  btwnlng3  28619  frgr3vlem2  30275  3vfriswmgr  30279  frgrregorufr0  30325  constrcccllem  33839  weiunso  36582  fnwe2lem3  43209  omcl2  43490  gpgprismgriedgdmss  48214  gpgedgvtx1  48224  gpgvtxedg0  48225  gpgvtxedg1  48226  gpg3kgrtriexlem6  48250  gpgprismgr4cycllem3  48259  eenglngeehlnmlem2  48900