Theorem 3mix1d 1343

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

Syntax hints:   → wi 4   ∨ w3o 1091

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 208  df-or 854  df-3or 1093

This theorem is referenced by:  f1dom3fv3dif  7212  f1dom3el3dif  7213  xpord3inddlem  8094  elfiun  9333  prinfzo0  13644  fvf1tp  13739  lcmfunsnlem2lem2  16599  estrreslem2  18095  ostth  27620  noextendlt  27651  ltssolem1  27657  nodense  27674  btwncolg1  28641  hlln  28693  btwnlng1  28705  constrllcllem  33936  colineartriv1  36295  weiunso  36694  fnwe2lem3  43497  dfxlim2v  46290  gpgprismgriedgdmss  48543  gpgedgvtx0  48552  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgprismgr4cycllem3  48588  eenglngeehlnmlem2  49229