Theorem 3mix3d 1334

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

Syntax hints:   → wi 4   ∨ w3o 1082

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 844  df-3or 1084

This theorem is referenced by:  elfiun  8893  nnnegz  11983  hashv01gt1  13704  lcmfunsnlem2lem2  15982  cshwshashlem1  16428  dyaddisjlem  24195  zabsle1  25871  btwncolg3  26342  btwnlng3  26406  frgr3vlem2  28052  3vfriswmgr  28056  frgrregorufr0  28102  noextendgt  33177  sltsolem1  33180  nodense  33196  fnwe2lem3  39650  eenglngeehlnmlem2  44724