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  4582  caofid0l  6271  caofid0r  6272  caofid1  6273  caofid2  6274  mapen  7075  fidcen  7131  fival  7212  supelti  7244  supmaxti  7246  infminti  7269  xnegdi  10147  frecuzrdgsuc  10722  hashunlem  11113  ccatrn  11235  ccatalpha  11239  swrdccat2  11301  pfxsuff1eqwrdeq  11329  ccatpfx  11331  swrdccatin2  11359  pfxccatin12lem2  11361  2zsupmax  11849  xrmin1inf  11890  serf0  11975  fsumabs  12089  binomlem  12107  cvgratz  12156  efcllemp  12282  ef0lem  12284  tannegap  12352  modm1div  12424  divalglemnqt  12544  bitsfzolem  12578  lcmid  12715  hashdvds  12856  prmdivdiv  12872  odzcllem  12878  reumodprminv  12889  nnnn0modprm0  12891  pythagtrip  12919  pcmpt  12979  pockthg  12993  4sqlem9  13022  4sqleminfi  13033  4sqexercise1  13034  4sqlem11  13037  ennnfonelemkh  13096  ctinf  13114  nninfdclemcl  13132  nninfdclemp1  13134  setsslid  13196  imasival  13452  imasaddflemg  13462  grpinvalem  13531  issubmnd  13588  imasmnd  13599  isgrpinv  13700  grpinvssd  13723  pwssub  13759  imasgrp  13761  mulgnndir  13801  subginv  13831  subginvcl  13833  ghmpreima  13916  conjnsg  13931  gsumsplit0  13996  srgidmlem  14055  ringidmlem  14099  imasring  14141  dvdsr01  14182  unitnegcl  14208  01eq0ring  14267  issubrng2  14288  subrginv  14315  subrgunit  14317  aprsym  14363  lmodvneg1  14409  lspsn  14495  isridlrng  14561  lidl0cl  14562  rspcl  14570  rspssid  14571  rnglidlmmgm  14575  2idlcpblrng  14602  quscrng  14612  rspsn  14613  znidom  14736  psrlinv  14768  psr1clfi  14772  topbas  14861  tgrest  14963  txss12  15060  mpomulcn  15360  cnplimclemle  15462  dvconstss  15492  efltlemlt  15568  coseq0q4123  15628  lgsval  15806  lgscllem  15809  gausslemma2dlem1a  15860  lgseisen  15876  lgsquadlem1  15879  lgsquadlem2  15880  2lgslem3a1  15899  2lgslem3b1  15900  2lgslem3c1  15901  2lgslem3d1  15902  2lgsoddprm  15915  uhgrspansubgrlem  16200  uspgr2wlkeq  16289  neapmkvlem  16783