Theorem 3mix2d 1350

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

Syntax hints:   → wi 4   ∨ w3o 1096

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 209  df-or 859  df-3or 1098

This theorem is referenced by:  sosn  5730  f1dom3fv3dif  7247  f1dom3el3dif  7248  xpord3inddlem  8128  elfiun  9370  fpwwe2lem12  10594  fvf1tp  13793  swrdnd0  14665  lcmfunsnlem2lem2  16664  dyaddisjlem  25645  ltssolem1  27727  tgcolg  28711  btwncolg2  28713  hlln  28764  btwnlng2  28777  frgrregorufr0  30483  constrsslem  33999  constrlccllem  34011  colineartriv2  36379  gpgprismgriedgdmss  48635  gpgvtxedg0  48646  gpgvtxedg1  48647  gpgedgiov  48648  eenglngeehlnmlem2  49321