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  7266  f1dom3el3dif  7267  xpord3inddlem  8158  elfiun  9447  prinfzo0  13720  fvf1tp  13811  lcmfunsnlem2lem2  16663  estrreslem2  18155  ostth  27607  noextendlt  27638  sltsolem1  27644  nodense  27661  btwncolg1  28539  hlln  28591  btwnlng1  28603  constrllcllem  33791  colineartriv1  36090  weiunso  36489  fnwe2lem3  43043  dfxlim2v  45843  gpgprismgriedgdmss  48023  gpgedgvtx0  48032  gpgvtxedg0  48034  gpgvtxedg1  48035  gpgprismgr4cycllem3  48063  eenglngeehlnmlem2  48685