Theorem 3mix1d 1355

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  f1dom3fv3dif  7266  f1dom3el3dif  7267  xpord3inddlem  8153  elfiun  9401  prinfzo0  13755  fvf1tp  13851  lcmfunsnlem2lem2  16730  estrreslem2  18227  ostth  27876  noextendlt  27906  ltssolem1  27912  nodense  27929  btwncolg1  28898  hlln  28953  btwnlng1  28967  elplnglnid  29141  constrllcllem  34263  colineartriv1  36648  weiunso  37086  fnwe2lem3  43894  dfxlim2v  46676  gpgprismgriedgdmss  48969  gpgedgvtx0  48978  gpgvtxedg0  48980  gpgvtxedg1  48981  gpgprismgr4cycllem3  49014  eenglngeehlnmlem2  49669