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  8158  elfiun  9447  nnnegz  12596  fvf1tp  13811  hashv01gt1  14368  lcmfunsnlem2lem2  16663  cshwshashlem1  17120  dyaddisjlem  25553  zabsle1  27264  noextendgt  27639  sltsolem1  27644  nodense  27661  btwncolg3  28541  btwnlng3  28605  frgr3vlem2  30260  3vfriswmgr  30264  frgrregorufr0  30310  constrcccllem  33793  weiunso  36489  fnwe2lem3  43043  omcl2  43324  gpgprismgriedgdmss  48023  gpgedgvtx1  48033  gpgvtxedg0  48034  gpgvtxedg1  48035  gpg3kgrtriexlem6  48057  gpgprismgr4cycllem3  48063  eenglngeehlnmlem2  48685