Theorem 3mix2d 1338

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 1332	. 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 849  df-3or 1088

This theorem is referenced by:  sosn  5772  f1dom3fv3dif  7288  f1dom3el3dif  7289  xpord3inddlem  8179  elfiun  9470  fpwwe2lem12  10682  fvf1tp  13829  swrdnd0  14695  lcmfunsnlem2lem2  16676  dyaddisjlem  25630  sltsolem1  27720  tgcolg  28562  btwncolg2  28564  hlln  28615  btwnlng2  28628  frgrregorufr0  30343  constrsslem  33782  colineartriv2  36069  gpgvtxedg0  48021  gpgvtxedg1  48022  eenglngeehlnmlem2  48659