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  8110  elfiun  9357  nnnegz  12508  fvf1tp  13727  hashv01gt1  14286  lcmfunsnlem2lem2  16585  cshwshashlem1  17042  dyaddisjlem  25472  zabsle1  27183  noextendgt  27558  sltsolem1  27563  nodense  27580  btwncolg3  28460  btwnlng3  28524  frgr3vlem2  30176  3vfriswmgr  30180  frgrregorufr0  30226  constrcccllem  33717  weiunso  36427  fnwe2lem3  43014  omcl2  43295  gpgprismgriedgdmss  48016  gpgedgvtx1  48026  gpgvtxedg0  48027  gpgvtxedg1  48028  gpg3kgrtriexlem6  48052  gpgprismgr4cycllem3  48060  eenglngeehlnmlem2  48700