Theorem syl2anr 290

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  swopo  4341  opswapg  5156  coexg  5214  iotass  5236  resdif  5526  fvexg  5577  isotr  5863  xpexgALT  6190  ixpssmapg  6787  mapen  6907  mapdom1g  6908  elfir  7039  cauappcvgprlemladdfl  7722  addgt0sr  7842  axmulass  7940  axdistr  7941  negeu  8217  ltaddnegr  8452  nnsub  9029  zltnle  9372  ltsubnn0  9393  elz2  9397  uzaddcl  9660  qaddcl  9709  xltneg  9911  xleneg  9912  iccneg  10064  uzsubsubfz  10122  fzsplit2  10125  fzss1  10138  uzsplit  10167  fz0fzdiffz0  10205  difelfzle  10209  difelfznle  10210  fzonlt0  10243  fzouzsplit  10255  eluzgtdifelfzo  10273  elfzodifsumelfzo  10277  ssfzo12  10300  qltnle  10333  modfzo0difsn  10487  nn0ennn  10525  seqfveq2g  10569  ser3mono  10579  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  seqf1oglem1  10611  seqf1oglem2  10612  seqf1og  10613  fser0const  10627  mulsubdivbinom2ap  10803  faclbnd  10833  bcval4  10844  bcpasc  10858  hashfacen  10928  seq3coll  10934  crim  11023  mingeb  11407  fsumshftm  11610  isumshft  11655  cvgratgt0  11698  mertenslemi1  11700  prod1dc  11751  fprod1p  11764  fprodmodd  11806  negdvdsb  11972  dvdsnegb  11973  dvdsmul1  11978  dvdsabseq  12012  dvdsssfz1  12017  odd2np1  12038  ndvdsadd  12096  dvdssqim  12191  nn0seqcvgd  12209  algcvgblem  12217  cncongr2  12272  prmind2  12288  prmdvdsfz  12307  prmndvdsfaclt  12324  dvdsfi  12407  modprm0  12423  modprmn0modprm0  12425  pythagtriplem1  12434  pythagtriplem4  12437  pythagtriplem8  12441  pythagtriplem9  12442  pythagtriplem12  12444  pythagtriplem14  12446  pythagtriplem16  12448  pcexp  12478  pc2dvds  12499  pcz  12501  fldivp1  12517  pcfac  12519  oddprmdvds  12523  pockthg  12526  infpnlem1  12528  1arith  12536  4sqlem11  12570  ismgmid  13020  mhmpropd  13098  grpsubid1  13217  mulgnnp1  13260  mulgsubcl  13266  mulgnn0z  13279  mulgnndir  13281  mulgneg2  13286  ghmco  13394  gsumfzfsumlemm  14143  resttopon  14407  cnovex  14432  iscn  14433  iscnp  14435  cnco  14457  cndis  14477  hmeoco  14552  bl2in  14639  metss2lem  14733  metss2  14734  bdxmet  14737  metrest  14742  ioo2bl  14787  expcn  14805  elcncf  14809  dvexp  14947  plypow  14980  relogexp  15108  logcxp  15133  wilthlem1  15216  sgmnncl  15224  mpodvdsmulf1o  15226  lgsdirnn0  15288  gausslemma2dlem1a  15299  lgsquadlem1  15318  lgsquad2  15324  lgsquad3  15325  supfz  15715