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 1085

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 848  df-3or 1087

This theorem is referenced by:  sosn  5698  f1dom3fv3dif  7197  f1dom3el3dif  7198  xpord3inddlem  8079  elfiun  9309  fpwwe2lem12  10528  fvf1tp  13688  swrdnd0  14560  lcmfunsnlem2lem2  16545  dyaddisjlem  25518  sltsolem1  27609  tgcolg  28527  btwncolg2  28529  hlln  28580  btwnlng2  28593  frgrregorufr0  30296  constrsslem  33746  constrlccllem  33758  colineartriv2  36102  gpgprismgriedgdmss  48083  gpgvtxedg0  48094  gpgvtxedg1  48095  gpgedgiov  48096  eenglngeehlnmlem2  48770