Theorem 3mix2d 1337

Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)

Hypothesis

Ref	Expression
3mixd.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
3mix2d	⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃))

Proof of Theorem 3mix2d

Step	Hyp	Ref	Expression
1		3mixd.1	. 2 ⊢ (𝜑 → 𝜓)
2		3mix2 1331	. 2 ⊢ (𝜓 → (𝜒 ∨ 𝜓 ∨ 𝜃))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃))

Syntax hints:   → wi 4   ∨ w3o 1086

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 847  df-3or 1088

This theorem is referenced by:  sosn  5786  f1dom3fv3dif  7305  f1dom3el3dif  7306  xpord3inddlem  8195  elfiun  9499  fpwwe2lem12  10711  fvf1tp  13840  swrdnd0  14705  lcmfunsnlem2lem2  16686  dyaddisjlem  25649  sltsolem1  27738  tgcolg  28580  btwncolg2  28582  hlln  28633  btwnlng2  28646  frgrregorufr0  30356  constrsslem  33731  colineartriv2  36032  eenglngeehlnmlem2  48472