Theorem 3mix3d 1355

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

Syntax hints:   → wi 4   ∨ w3o 1100

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 210  df-or 861  df-3or 1102

This theorem is referenced by:  xpord3inddlem  8146  elfiun  9386  nnnegz  12590  fvf1tp  13818  hashv01gt1  14377  lcmfunsnlem2lem2  16693  cshwshashlem1  17151  dyaddisjlem  25719  zabsle1  27422  noextendgt  27796  ltssolem1  27801  nodense  27818  btwncolg3  28788  btwnlng3  28852  frgr3vlem2  30562  3vfriswmgr  30566  frgrregorufr0  30612  constrcccllem  34085  weiunso  36862  fnwe2lem3  43666  omcl2  43947  gpgprismgriedgdmss  48701  gpgedgvtx1  48711  gpgvtxedg0  48712  gpgvtxedg1  48713  gpg3kgrtriexlem6  48737  gpgprismgr4cycllem3  48746  eenglngeehlnmlem2  49398