Theorem syl2an2r 595

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 578	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  4481  mapen  6848  fival  6971  supelti  7003  supmaxti  7005  infminti  7028  xnegdi  9870  frecuzrdgsuc  10416  hashunlem  10786  2zsupmax  11236  xrmin1inf  11277  serf0  11362  fsumabs  11475  binomlem  11493  cvgratz  11542  efcllemp  11668  ef0lem  11670  tannegap  11738  modm1div  11809  divalglemnqt  11927  lcmid  12082  hashdvds  12223  prmdivdiv  12239  odzcllem  12244  reumodprminv  12255  nnnn0modprm0  12257  pythagtrip  12285  pcmpt  12343  pockthg  12357  4sqlem9  12386  ennnfonelemkh  12415  ctinf  12433  nninfdclemp1  12453  setsslid  12515  imasival  12732  imasaddflemg  12742  grprinvlem  12809  issubmnd  12848  isgrpinv  12931  grpinvssd  12952  mulgnndir  13017  subginv  13046  subginvcl  13048  srgidmlem  13166  ringidmlem  13210  dvdsr01  13278  unitnegcl  13304  01eq0ring  13335  subrginv  13363  subrgunit  13365  aprsym  13379  lmodvneg1  13425  lspsn  13507  topbas  13652  tgrest  13754  txss12  13851  cnplimclemle  14222  efltlemlt  14280  coseq0q4123  14340  lgsval  14490  lgscllem  14493  neapmkvlem  14900