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:  xpord3inddlem  8152  elfiun  9393  nnnegz  12605  fvf1tp  13836  hashv01gt1  14395  lcmfunsnlem2lem2  16715  cshwshashlem1  17173  dyaddisjlem  25785  zabsle1  27491  noextendgt  27865  ltssolem1  27870  nodense  27887  btwncolg3  28857  btwnlng3  28925  frgr3vlem2  30672  3vfriswmgr  30676  frgrregorufr0  30722  constrcccllem  34184  weiunso  37010  fnwe2lem3  43812  omcl2  44093  gpgprismgriedgdmss  48850  gpgedgvtx1  48860  gpgvtxedg0  48861  gpgvtxedg1  48862  gpg3kgrtriexlem6  48886  gpgprismgr4cycllem3  48895  eenglngeehlnmlem2  49551