Theorem syl2an2r 597

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  4569  caofid0l  6243  caofid0r  6244  caofid1  6245  caofid2  6246  mapen  7003  fival  7133  supelti  7165  supmaxti  7167  infminti  7190  xnegdi  10060  frecuzrdgsuc  10631  hashunlem  11021  ccatrn  11139  swrdccat2  11198  pfxsuff1eqwrdeq  11226  ccatpfx  11228  swrdccatin2  11256  pfxccatin12lem2  11258  2zsupmax  11732  xrmin1inf  11773  serf0  11858  fsumabs  11971  binomlem  11989  cvgratz  12038  efcllemp  12164  ef0lem  12166  tannegap  12234  modm1div  12306  divalglemnqt  12426  bitsfzolem  12460  lcmid  12597  hashdvds  12738  prmdivdiv  12754  odzcllem  12760  reumodprminv  12771  nnnn0modprm0  12773  pythagtrip  12801  pcmpt  12861  pockthg  12875  4sqlem9  12904  4sqleminfi  12915  4sqexercise1  12916  4sqlem11  12919  ennnfonelemkh  12978  ctinf  12996  nninfdclemcl  13014  nninfdclemp1  13016  setsslid  13078  imasival  13334  imasaddflemg  13344  grpinvalem  13413  issubmnd  13470  imasmnd  13481  isgrpinv  13582  grpinvssd  13605  pwssub  13641  imasgrp  13643  mulgnndir  13683  subginv  13713  subginvcl  13715  ghmpreima  13798  conjnsg  13813  srgidmlem  13936  ringidmlem  13980  imasring  14022  dvdsr01  14062  unitnegcl  14088  01eq0ring  14147  issubrng2  14168  subrginv  14195  subrgunit  14197  aprsym  14242  lmodvneg1  14288  lspsn  14374  isridlrng  14440  lidl0cl  14441  rspcl  14449  rspssid  14450  rnglidlmmgm  14454  2idlcpblrng  14481  quscrng  14491  rspsn  14492  znidom  14615  psrlinv  14642  psr1clfi  14646  topbas  14735  tgrest  14837  txss12  14934  mpomulcn  15234  cnplimclemle  15336  dvconstss  15366  efltlemlt  15442  coseq0q4123  15502  lgsval  15677  lgscllem  15680  gausslemma2dlem1a  15731  lgseisen  15747  lgsquadlem1  15750  lgsquadlem2  15751  2lgslem3a1  15770  2lgslem3b1  15771  2lgslem3c1  15772  2lgslem3d1  15773  2lgsoddprm  15786  neapmkvlem  16394