Theorem syl2anr 284

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 283	. 2 |- ( ( ph /\ ta ) -> th )
5	4	ancoms 264	1 |- ( ( ta /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  swopo  4061  opswapg  4827  coexg  4882  iotass  4904  resdif  5168  fvexg  5214  isotr  5476  xpexgALT  5780  cauappcvgprlemladdfl  6845  addgt0sr  6952  axmulass  7039  axdistr  7040  negeu  7299  ltaddnegr  7529  nnsub  8077  zltnle  8397  elz2  8419  uzaddcl  8674  qaddcl  8720  xltneg  8903  xleneg  8904  iccneg  9011  uzsubsubfz  9066  fzsplit2  9069  fzss1  9081  uzsplit  9109  fz0fzdiffz0  9141  difelfzle  9145  difelfznle  9146  fzonlt0  9176  fzouzsplit  9188  eluzgtdifelfzo  9206  elfzodifsumelfzo  9210  ssfzo12  9233  qltnle  9255  modfzo0difsn  9397  nn0ennn  9425  isermono  9457  faclbnd  9668  bcval4  9679  bcpasc  9693  crim  9745  negdvdsb  10211  dvdsnegb  10212  dvdsmul1  10217  dvdsabseq  10247  dvdsssfz1  10252  odd2np1  10272  ndvdsadd  10331  dvdssqim  10413  nn0seqcvgd  10423  algcvgblem  10431  cncongr2  10486  prmind2  10502  prmdvdsfz  10520  prmndvdsfaclt  10535