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  6261  caofid0r  6262  caofid1  6263  caofid2  6264  mapen  7031  fidcen  7087  fival  7168  supelti  7200  supmaxti  7202  infminti  7225  xnegdi  10102  frecuzrdgsuc  10675  hashunlem  11066  ccatrn  11185  ccatalpha  11189  swrdccat2  11251  pfxsuff1eqwrdeq  11279  ccatpfx  11281  swrdccatin2  11309  pfxccatin12lem2  11311  2zsupmax  11786  xrmin1inf  11827  serf0  11912  fsumabs  12025  binomlem  12043  cvgratz  12092  efcllemp  12218  ef0lem  12220  tannegap  12288  modm1div  12360  divalglemnqt  12480  bitsfzolem  12514  lcmid  12651  hashdvds  12792  prmdivdiv  12808  odzcllem  12814  reumodprminv  12825  nnnn0modprm0  12827  pythagtrip  12855  pcmpt  12915  pockthg  12929  4sqlem9  12958  4sqleminfi  12969  4sqexercise1  12970  4sqlem11  12973  ennnfonelemkh  13032  ctinf  13050  nninfdclemcl  13068  nninfdclemp1  13070  setsslid  13132  imasival  13388  imasaddflemg  13398  grpinvalem  13467  issubmnd  13524  imasmnd  13535  isgrpinv  13636  grpinvssd  13659  pwssub  13695  imasgrp  13697  mulgnndir  13737  subginv  13767  subginvcl  13769  ghmpreima  13852  conjnsg  13867  srgidmlem  13990  ringidmlem  14034  imasring  14076  dvdsr01  14117  unitnegcl  14143  01eq0ring  14202  issubrng2  14223  subrginv  14250  subrgunit  14252  aprsym  14297  lmodvneg1  14343  lspsn  14429  isridlrng  14495  lidl0cl  14496  rspcl  14504  rspssid  14505  rnglidlmmgm  14509  2idlcpblrng  14536  quscrng  14546  rspsn  14547  znidom  14670  psrlinv  14697  psr1clfi  14701  topbas  14790  tgrest  14892  txss12  14989  mpomulcn  15289  cnplimclemle  15391  dvconstss  15421  efltlemlt  15497  coseq0q4123  15557  lgsval  15732  lgscllem  15735  gausslemma2dlem1a  15786  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  2lgslem3a1  15825  2lgslem3b1  15826  2lgslem3c1  15827  2lgslem3d1  15828  2lgsoddprm  15841  uhgrspansubgrlem  16126  uspgr2wlkeq  16215  neapmkvlem  16671