Theorem 3mix3d 1338

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

Syntax hints:   → wi 4   ∨ w3o 1086

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 847  df-3or 1088

This theorem is referenced by:  xpord3inddlem  8195  elfiun  9499  nnnegz  12642  fvf1tp  13840  hashv01gt1  14394  lcmfunsnlem2lem2  16686  cshwshashlem1  17143  dyaddisjlem  25649  zabsle1  27358  noextendgt  27733  sltsolem1  27738  nodense  27755  btwncolg3  28583  btwnlng3  28647  frgr3vlem2  30306  3vfriswmgr  30310  frgrregorufr0  30356  weiunso  36432  fnwe2lem3  43009  omcl2  43295  eenglngeehlnmlem2  48472