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  4627  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  mapen  7152  fidcen  7209  fival  7309  supelti  7348  supmaxti  7350  infminti  7373  xnegdi  10286  fzsplit3  10474  frecuzrdgsuc  10871  nn0sqdc  11167  hashunlem  11265  ccatrn  11398  ccatalpha  11402  swrdccat2  11464  pfxsuff1eqwrdeq  11492  ccatpfx  11494  swrdccatin2  11522  pfxccatin12lem2  11524  2zsupmax  12014  xrmin1inf  12057  serf0  12142  fsumabs  12256  binomlem  12274  cvgratz  12323  efcllemp  12449  ef0lem  12451  tannegap  12519  modm1div  12591  divalglemnqt  12711  bitsfzolem  12745  lcmid  12882  pwbdvdseulemle  12970  hashdvds  13027  prmdivdiv  13043  odzcllem  13049  reumodprminv  13060  nnnn0modprm0  13062  pythagtrip  13090  pcmpt  13150  pockthg  13164  4sqlem9  13193  4sqleminfi  13204  4sqexercise1  13205  4sqlem11  13208  ballotfilemic  13307  ballotfilemrv2  13322  ennnfonelemkh  13360  ctinf  13378  nninfdclemcl  13396  nninfdclemp1  13398  setsslid  13460  imasival  13685  imasaddflemg  13695  grpinvalem  13763  issubmnd  13813  imasmnd  13818  isgrpinv  13917  grpinvssd  13940  imasgrp  13972  mulgnndir  14012  subginv  14042  subginvcl  14044  ghmpreima  14127  conjnsg  14142  gzsumsplit0  14237  gsumconstcmn  14265  pwssub  14322  srgidmlem  14388  ringidmlem  14433  imasring  14477  dvdsr01  14519  unitnegcl  14545  01eq0ring  14604  issubrng2  14626  subrginv  14653  subrgunit  14655  aprsym  14704  lmodvneg1  14775  lspsn  14861  isridlrng  14927  lidl0cl  14928  rspcl  14936  rspssid  14937  rnglidlmmgm  14941  2idlcpblrng  14968  quscrng  14978  rspsn  14979  znidom  15100  psrlinv  15203  psr1clfi  15207  topbas  15310  tgrest  15412  txss12  15509  mpomulcn  15809  cnplimclemle  15911  dvconstss  15941  efltlemlt  16017  coseq0q4123  16078  chtqub  16313  bposlem2  16329  lgsval  16345  lgscllem  16348  gausslemma2dlem1a  16399  lgseisen  16415  lgsquadlem1  16418  lgsquadlem2  16419  2lgslem3a1  16438  2lgslem3b1  16439  2lgslem3c1  16440  2lgslem3d1  16441  2lgsoddprm  16454  uhgrspansubgrlem  16739  uspgr2wlkeq  16828  neapmkvlem  17341