Theorem 3mix2d 1335

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

Syntax hints:   → wi 4   ∨ w3o 1084

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 844  df-3or 1086

This theorem is referenced by:  sosn  5664  f1dom3fv3dif  7122  f1dom3el3dif  7123  elfiun  9119  fpwwe2lem12  10329  swrdnd0  14298  lcmfunsnlem2lem2  16272  dyaddisjlem  24664  tgcolg  26819  btwncolg2  26821  hlln  26872  btwnlng2  26885  frgrregorufr0  28589  xpord3ind  33727  sltsolem1  33805  colineartriv2  34297  eenglngeehlnmlem2  45972