Theorem syl2anr 274

Description: A double syllogism inference. (Contributed by NM, 17-Sep-2013.)

Hypotheses

Ref	Expression
syl2an.1	|- ( ph -> ps )
syl2an.2	|- ( ta -> ch )
syl2an.3	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
syl2anr	|- ( ( ta /\ ph ) -> th )

Proof of Theorem syl2anr

Step	Hyp	Ref	Expression
1		syl2an.1	. . 3 |- ( ph -> ps )
2		syl2an.2	. . 3 |- ( ta -> ch )
3		syl2an.3	. . 3 |- ( ( ps /\ ch ) -> th )
4	1, 2, 3	syl2an 273	. 2 |- ( ( ph /\ ta ) -> th )
5	4	ancoms 255	1 |- ( ( ta /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  swopo  4043  opswapg  4807  coexg  4862  iotass  4884  resdif  5148  fvexg  5194  isotr  5456  xpexgALT  5760  cauappcvgprlemladdfl  6753  addgt0sr  6860  axmulass  6947  axdistr  6948  negeu  7202  nnsub  7952  zltnle  8291  elz2  8312  uzaddcl  8529  qaddcl  8570  xltneg  8749  xleneg  8750  iccneg  8857  uzsubsubfz  8911  fzsplit2  8914  fzss1  8926  uzsplit  8954  fz0fzdiffz0  8987  difelfzle  8992  difelfznle  8993  fzonlt0  9023  fzouzsplit  9035  eluzgtdifelfzo  9053  elfzodifsumelfzo  9057  ssfzo12  9080  qltnle  9101  nn0ennn  9209  isermono  9237  crim  9458  nn0seqcvgd  9880  algcvgblem  9888