Theorem 3mix2d 1229

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

Syntax hints:   → wi 4   ∨ w3o 1029

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 195  df-or 383  df-3or 1031

This theorem is referenced by:  sosn  5100  funtpgOLD  5842  f1dom3fv3dif  6402  f1dom3el3dif  6403  elfiun  8196  fpwwe2lem13  9320  lcmfunsnlem2lem2  15138  dyaddisjlem  23113  tgcolg  25194  btwncolg2  25196  hlln  25247  btwnlng2  25260  frgraregorufr0  26372  sltsolem1  30860  colineartriv2  31138  frgrregorufr0  41470