Theorem syl2anr 288

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  swopo  4291  opswapg  5097  coexg  5155  iotass  5177  resdif  5464  fvexg  5515  isotr  5795  xpexgALT  6112  ixpssmapg  6706  mapen  6824  mapdom1g  6825  elfir  6950  cauappcvgprlemladdfl  7617  addgt0sr  7737  axmulass  7835  axdistr  7836  negeu  8110  ltaddnegr  8344  nnsub  8917  zltnle  9258  ltsubnn0  9279  elz2  9283  uzaddcl  9545  qaddcl  9594  xltneg  9793  xleneg  9794  iccneg  9946  uzsubsubfz  10003  fzsplit2  10006  fzss1  10019  uzsplit  10048  fz0fzdiffz0  10086  difelfzle  10090  difelfznle  10091  fzonlt0  10123  fzouzsplit  10135  eluzgtdifelfzo  10153  elfzodifsumelfzo  10157  ssfzo12  10180  qltnle  10202  modfzo0difsn  10351  nn0ennn  10389  ser3mono  10434  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  fser0const  10472  faclbnd  10675  bcval4  10686  bcpasc  10700  hashfacen  10771  seq3coll  10777  crim  10822  mingeb  11205  fsumshftm  11408  isumshft  11453  cvgratgt0  11496  mertenslemi1  11498  prod1dc  11549  fprod1p  11562  fprodmodd  11604  negdvdsb  11769  dvdsnegb  11770  dvdsmul1  11775  dvdsabseq  11807  dvdsssfz1  11812  odd2np1  11832  ndvdsadd  11890  dvdssqim  11979  nn0seqcvgd  11995  algcvgblem  12003  cncongr2  12058  prmind2  12074  prmdvdsfz  12093  prmndvdsfaclt  12110  phisum  12194  modprm0  12208  modprmn0modprm0  12210  pythagtriplem1  12219  pythagtriplem4  12222  pythagtriplem8  12226  pythagtriplem9  12227  pythagtriplem12  12229  pythagtriplem14  12231  pythagtriplem16  12233  pcexp  12263  pc2dvds  12283  pcz  12285  fldivp1  12300  pcfac  12302  oddprmdvds  12306  pockthg  12309  infpnlem1  12311  1arith  12319  ismgmid  12631  mhmpropd  12689  resttopon  12965  cnovex  12990  iscn  12991  iscnp  12993  cnco  13015  cndis  13035  hmeoco  13110  bl2in  13197  metss2lem  13291  metss2  13292  bdxmet  13295  metrest  13300  ioo2bl  13337  elcncf  13354  dvexp  13469  relogexp  13587  logcxp  13612  lgsdirnn0  13742  supfz  14100