Theorem 3mix2d 1334

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

Syntax hints:   → wi 4   ∨ w3o 1083

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 206  df-or 846  df-3or 1085

This theorem is referenced by:  sosn  5768  f1dom3fv3dif  7283  f1dom3el3dif  7284  xpord3inddlem  8168  elfiun  9473  fpwwe2lem12  10685  swrdnd0  14665  lcmfunsnlem2lem2  16640  dyaddisjlem  25615  sltsolem1  27705  tgcolg  28481  btwncolg2  28483  hlln  28534  btwnlng2  28547  frgrregorufr0  30257  constrsslem  33599  colineartriv2  35892  eenglngeehlnmlem2  48126