Theorem syl2an2r 599

Description: syl2anr 290 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)

Hypotheses

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

Assertion

Ref	Expression
syl2an2r	|- ( ( ph /\ ch ) -> ta )

Proof of Theorem syl2an2r

Step	Hyp	Ref	Expression
1		syl2an2r.1	. . 3 |- ( ph -> ps )
2		syl2an2r.2	. . 3 |- ( ( ph /\ ch ) -> th )
3		syl2an2r.3	. . 3 |- ( ( ps /\ th ) -> ta )
4	1, 2, 3	syl2an 289	. 2 |- ( ( ph /\ ( ph /\ ch ) ) -> ta )
5	4	anabss5 580	1 |- ( ( ph /\ ch ) -> ta )

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 depends on definitions:  df-bi 117

This theorem is referenced by:  op1stbg  4576  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  mapen  7032  fidcen  7088  fival  7169  supelti  7201  supmaxti  7203  infminti  7226  xnegdi  10103  frecuzrdgsuc  10677  hashunlem  11068  ccatrn  11190  ccatalpha  11194  swrdccat2  11256  pfxsuff1eqwrdeq  11284  ccatpfx  11286  swrdccatin2  11314  pfxccatin12lem2  11316  2zsupmax  11791  xrmin1inf  11832  serf0  11917  fsumabs  12031  binomlem  12049  cvgratz  12098  efcllemp  12224  ef0lem  12226  tannegap  12294  modm1div  12366  divalglemnqt  12486  bitsfzolem  12520  lcmid  12657  hashdvds  12798  prmdivdiv  12814  odzcllem  12820  reumodprminv  12831  nnnn0modprm0  12833  pythagtrip  12861  pcmpt  12921  pockthg  12935  4sqlem9  12964  4sqleminfi  12975  4sqexercise1  12976  4sqlem11  12979  ennnfonelemkh  13038  ctinf  13056  nninfdclemcl  13074  nninfdclemp1  13076  setsslid  13138  imasival  13394  imasaddflemg  13404  grpinvalem  13473  issubmnd  13530  imasmnd  13541  isgrpinv  13642  grpinvssd  13665  pwssub  13701  imasgrp  13703  mulgnndir  13743  subginv  13773  subginvcl  13775  ghmpreima  13858  conjnsg  13873  gsumsplit0  13938  srgidmlem  13997  ringidmlem  14041  imasring  14083  dvdsr01  14124  unitnegcl  14150  01eq0ring  14209  issubrng2  14230  subrginv  14257  subrgunit  14259  aprsym  14304  lmodvneg1  14350  lspsn  14436  isridlrng  14502  lidl0cl  14503  rspcl  14511  rspssid  14512  rnglidlmmgm  14516  2idlcpblrng  14543  quscrng  14553  rspsn  14554  znidom  14677  psrlinv  14704  psr1clfi  14708  topbas  14797  tgrest  14899  txss12  14996  mpomulcn  15296  cnplimclemle  15398  dvconstss  15428  efltlemlt  15504  coseq0q4123  15564  lgsval  15739  lgscllem  15742  gausslemma2dlem1a  15793  lgseisen  15809  lgsquadlem1  15812  lgsquadlem2  15813  2lgslem3a1  15832  2lgslem3b1  15833  2lgslem3c1  15834  2lgslem3d1  15835  2lgsoddprm  15848  uhgrspansubgrlem  16133  uspgr2wlkeq  16222  neapmkvlem  16698