Theorem 3mix1d 1353

Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)

Hypothesis

Ref	Expression
3mixd.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
3mix1d	⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃))

Proof of Theorem 3mix1d

Step	Hyp	Ref	Expression
1		3mixd.1	. 2 ⊢ (𝜑 → 𝜓)
2		3mix1 1347	. 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:  f1dom3fv3dif  7267  f1dom3el3dif  7268  xpord3inddlem  8149  elfiun  9389  prinfzo0  13726  fvf1tp  13821  lcmfunsnlem2lem2  16696  estrreslem2  18193  ostth  27768  noextendlt  27798  ltssolem1  27804  nodense  27821  btwncolg1  28789  hlln  28841  btwnlng1  28853  elplnglnid  29022  constrllcllem  34086  colineartriv1  36457  weiunso  36865  fnwe2lem3  43670  dfxlim2v  46452  gpgprismgriedgdmss  48705  gpgedgvtx0  48714  gpgvtxedg0  48716  gpgvtxedg1  48717  gpgprismgr4cycllem3  48750  eenglngeehlnmlem2  49402