Theorem 3mix1d 1236

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

Syntax hints:   → wi 4   ∨ w3o 1036

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 197  df-or 385  df-3or 1038

This theorem is referenced by:  f1dom3fv3dif  6525  f1dom3el3dif  6526  elfiun  8336  prinfzo0  12506  lcmfunsnlem2lem2  15352  estrreslem2  16778  ostth  25328  btwncolg1  25450  hlln  25502  btwnlng1  25514  noextendlt  31822  sltsolem1  31826  nodense  31842  colineartriv1  32174  fnwe2lem3  37622  dfxlim2v  40073