Theorem 3mix3d 1351

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

Syntax hints:   → wi 4   ∨ w3o 1096

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 209  df-or 859  df-3or 1098

This theorem is referenced by:  xpord3inddlem  8128  elfiun  9370  nnnegz  12565  fvf1tp  13793  hashv01gt1  14352  lcmfunsnlem2lem2  16664  cshwshashlem1  17122  dyaddisjlem  25645  zabsle1  27348  noextendgt  27722  ltssolem1  27727  nodense  27744  btwncolg3  28714  btwnlng3  28778  frgr3vlem2  30433  3vfriswmgr  30437  frgrregorufr0  30483  constrcccllem  34012  weiunso  36787  fnwe2lem3  43590  omcl2  43871  gpgprismgriedgdmss  48635  gpgedgvtx1  48645  gpgvtxedg0  48646  gpgvtxedg1  48647  gpg3kgrtriexlem6  48671  gpgprismgr4cycllem3  48680  eenglngeehlnmlem2  49321