Theorem 3mix1d 1354

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

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

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 861  df-3or 1103

This theorem is used by:  f1dom3fv3dif  7266  f1dom3el3dif  7267  xpord3inddlem  8148  elfiun  9388  prinfzo0  13734  fvf1tp  13829  lcmfunsnlem2lem2  16703  estrreslem2  18200  ostth  27814  noextendlt  27844  ltssolem1  27850  nodense  27867  btwncolg1  28835  hlln  28890  btwnlng1  28903  elplnglnid  29076  constrllcllem  34151  colineartriv1  36567  weiunso  37005  fnwe2lem3  43807  dfxlim2v  46589  gpgprismgriedgdmss  48845  gpgedgvtx0  48854  gpgvtxedg0  48856  gpgvtxedg1  48857  gpgprismgr4cycllem3  48890  eenglngeehlnmlem2  49546