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  7225  f1dom3el3dif  7226  xpord3inddlem  8110  elfiun  9357  prinfzo0  13635  fvf1tp  13727  lcmfunsnlem2lem2  16585  estrreslem2  18079  ostth  27583  noextendlt  27614  sltsolem1  27620  nodense  27637  btwncolg1  28535  hlln  28587  btwnlng1  28599  constrllcllem  33735  colineartriv1  36048  weiunso  36447  fnwe2lem3  43034  dfxlim2v  45838  gpgprismgriedgdmss  48036  gpgedgvtx0  48045  gpgvtxedg0  48047  gpgvtxedg1  48048  gpgprismgr4cycllem3  48080  eenglngeehlnmlem2  48720