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  4605  caofid0l  6302  caofid0r  6303  caofid1  6304  caofid2  6305  mapen  7112  fidcen  7169  fival  7270  supelti  7306  supmaxti  7308  infminti  7331  xnegdi  10220  fzsplit3  10407  frecuzrdgsuc  10800  hashunlem  11193  ccatrn  11322  ccatalpha  11326  swrdccat2  11388  pfxsuff1eqwrdeq  11416  ccatpfx  11418  swrdccatin2  11446  pfxccatin12lem2  11448  2zsupmax  11936  xrmin1inf  11977  serf0  12062  fsumabs  12176  binomlem  12194  cvgratz  12243  efcllemp  12369  ef0lem  12371  tannegap  12439  modm1div  12511  divalglemnqt  12631  bitsfzolem  12665  lcmid  12802  hashdvds  12943  prmdivdiv  12959  odzcllem  12965  reumodprminv  12976  nnnn0modprm0  12978  pythagtrip  13006  pcmpt  13066  pockthg  13080  4sqlem9  13109  4sqleminfi  13120  4sqexercise1  13121  4sqlem11  13124  ballotfilemic  13194  ballotfilemrv2  13209  ennnfonelemkh  13247  ctinf  13265  nninfdclemcl  13283  nninfdclemp1  13285  setsslid  13347  imasival  13570  imasaddflemg  13580  grpinvalem  13648  issubmnd  13703  imasmnd  13708  isgrpinv  13809  grpinvssd  13832  imasgrp  13864  mulgnndir  13904  subginv  13934  subginvcl  13936  ghmpreima  14019  conjnsg  14034  gsumsplit0  14099  pwssub  14158  srgidmlem  14221  ringidmlem  14265  imasring  14307  dvdsr01  14349  unitnegcl  14375  01eq0ring  14434  issubrng2  14456  subrginv  14483  subrgunit  14485  aprsym  14534  lmodvneg1  14604  lspsn  14690  isridlrng  14756  lidl0cl  14757  rspcl  14765  rspssid  14766  rnglidlmmgm  14770  2idlcpblrng  14797  quscrng  14807  rspsn  14808  znidom  14931  psrlinv  14965  psr1clfi  14969  topbas  15058  tgrest  15160  txss12  15257  mpomulcn  15557  cnplimclemle  15659  dvconstss  15689  efltlemlt  15765  coseq0q4123  15825  lgsval  16003  lgscllem  16006  gausslemma2dlem1a  16057  lgseisen  16073  lgsquadlem1  16076  lgsquadlem2  16077  2lgslem3a1  16096  2lgslem3b1  16097  2lgslem3c1  16098  2lgslem3d1  16099  2lgsoddprm  16112  uhgrspansubgrlem  16397  uspgr2wlkeq  16486  neapmkvlem  16979