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  4600  caofid0l  6293  caofid0r  6294  caofid1  6295  caofid2  6296  mapen  7099  fidcen  7156  fival  7257  supelti  7293  supmaxti  7295  infminti  7318  xnegdi  10201  frecuzrdgsuc  10776  hashunlem  11168  ccatrn  11297  ccatalpha  11301  swrdccat2  11363  pfxsuff1eqwrdeq  11391  ccatpfx  11393  swrdccatin2  11421  pfxccatin12lem2  11423  2zsupmax  11911  xrmin1inf  11952  serf0  12037  fsumabs  12151  binomlem  12169  cvgratz  12218  efcllemp  12344  ef0lem  12346  tannegap  12414  modm1div  12486  divalglemnqt  12606  bitsfzolem  12640  lcmid  12777  hashdvds  12918  prmdivdiv  12934  odzcllem  12940  reumodprminv  12951  nnnn0modprm0  12953  pythagtrip  12981  pcmpt  13041  pockthg  13055  4sqlem9  13084  4sqleminfi  13095  4sqexercise1  13096  4sqlem11  13099  ennnfonelemkh  13163  ctinf  13181  nninfdclemcl  13199  nninfdclemp1  13201  setsslid  13263  imasival  13519  imasaddflemg  13529  grpinvalem  13598  issubmnd  13655  imasmnd  13666  isgrpinv  13767  grpinvssd  13790  pwssub  13826  imasgrp  13828  mulgnndir  13868  subginv  13898  subginvcl  13900  ghmpreima  13983  conjnsg  13998  gsumsplit0  14063  srgidmlem  14122  ringidmlem  14166  imasring  14208  dvdsr01  14249  unitnegcl  14275  01eq0ring  14334  issubrng2  14355  subrginv  14382  subrgunit  14384  aprsym  14430  lmodvneg1  14478  lspsn  14564  isridlrng  14630  lidl0cl  14631  rspcl  14639  rspssid  14640  rnglidlmmgm  14644  2idlcpblrng  14671  quscrng  14681  rspsn  14682  znidom  14805  psrlinv  14839  psr1clfi  14843  topbas  14932  tgrest  15034  txss12  15131  mpomulcn  15431  cnplimclemle  15533  dvconstss  15563  efltlemlt  15639  coseq0q4123  15699  lgsval  15877  lgscllem  15880  gausslemma2dlem1a  15931  lgseisen  15947  lgsquadlem1  15950  lgsquadlem2  15951  2lgslem3a1  15970  2lgslem3b1  15971  2lgslem3c1  15972  2lgslem3d1  15973  2lgsoddprm  15986  uhgrspansubgrlem  16271  uspgr2wlkeq  16360  neapmkvlem  16853