Theorem syl2an2r 603

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 584	1 |- ( ( ph /\ ch ) -> ta )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  op1stbg  4625  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  mapen  7146  fidcen  7203  fival  7304  supelti  7343  supmaxti  7345  infminti  7368  xnegdi  10281  fzsplit3  10469  frecuzrdgsuc  10866  nn0sqdc  11162  hashunlem  11260  ccatrn  11393  ccatalpha  11397  swrdccat2  11459  pfxsuff1eqwrdeq  11487  ccatpfx  11489  swrdccatin2  11517  pfxccatin12lem2  11519  2zsupmax  12009  xrmin1inf  12052  serf0  12137  fsumabs  12251  binomlem  12269  cvgratz  12318  efcllemp  12444  ef0lem  12446  tannegap  12514  modm1div  12586  divalglemnqt  12706  bitsfzolem  12740  lcmid  12877  pwbdvdseulemle  12965  hashdvds  13022  prmdivdiv  13038  odzcllem  13044  reumodprminv  13055  nnnn0modprm0  13057  pythagtrip  13085  pcmpt  13145  pockthg  13159  4sqlem9  13188  4sqleminfi  13199  4sqexercise1  13200  4sqlem11  13203  ballotfilemic  13302  ballotfilemrv2  13317  ennnfonelemkh  13355  ctinf  13373  nninfdclemcl  13391  nninfdclemp1  13393  setsslid  13455  imasival  13680  imasaddflemg  13690  grpinvalem  13758  issubmnd  13808  imasmnd  13813  isgrpinv  13912  grpinvssd  13935  imasgrp  13967  mulgnndir  14007  subginv  14037  subginvcl  14039  ghmpreima  14122  conjnsg  14137  gzsumsplit0  14232  gsumconstcmn  14250  pwssub  14300  srgidmlem  14366  ringidmlem  14411  imasring  14453  dvdsr01  14495  unitnegcl  14521  01eq0ring  14580  issubrng2  14602  subrginv  14629  subrgunit  14631  aprsym  14680  lmodvneg1  14751  lspsn  14837  isridlrng  14903  lidl0cl  14904  rspcl  14912  rspssid  14913  rnglidlmmgm  14917  2idlcpblrng  14944  quscrng  14954  rspsn  14955  znidom  15076  psrlinv  15166  psr1clfi  15170  topbas  15259  tgrest  15361  txss12  15458  mpomulcn  15758  cnplimclemle  15860  dvconstss  15890  efltlemlt  15966  coseq0q4123  16027  chtqub  16257  bposlem2  16273  lgsval  16289  lgscllem  16292  gausslemma2dlem1a  16343  lgseisen  16359  lgsquadlem1  16362  lgsquadlem2  16363  2lgslem3a1  16382  2lgslem3b1  16383  2lgslem3c1  16384  2lgslem3d1  16385  2lgsoddprm  16398  uhgrspansubgrlem  16683  uspgr2wlkeq  16772  neapmkvlem  17284