Theorem 3mix2d 1230

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

Syntax hints:   → wi 4   ∨ w3o 1030

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 196  df-or 384  df-3or 1032

This theorem is referenced by:  sosn  5111  funtpgOLD  5857  f1dom3fv3dif  6425  f1dom3el3dif  6426  elfiun  8219  fpwwe2lem13  9343  lcmfunsnlem2lem2  15190  dyaddisjlem  23169  tgcolg  25249  btwncolg2  25251  hlln  25302  btwnlng2  25315  frgraregorufr0  26579  sltsolem1  31067  colineartriv2  31345  frgrregorufr0  41489