Theorem 3mix1d 1337

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

Syntax hints:   → wi 4   ∨ w3o 1085

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 848  df-3or 1087

This theorem is referenced by:  f1dom3fv3dif  7205  f1dom3el3dif  7206  xpord3inddlem  8087  elfiun  9320  prinfzo0  13601  fvf1tp  13693  lcmfunsnlem2lem2  16550  estrreslem2  18044  ostth  27548  noextendlt  27579  sltsolem1  27585  nodense  27602  btwncolg1  28500  hlln  28552  btwnlng1  28564  constrllcllem  33719  colineartriv1  36041  weiunso  36440  fnwe2lem3  43025  dfxlim2v  45828  gpgprismgriedgdmss  48036  gpgedgvtx0  48045  gpgvtxedg0  48047  gpgvtxedg1  48048  gpgprismgr4cycllem3  48081  eenglngeehlnmlem2  48723