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  4526  caofid0l  6185  caofid0r  6186  caofid1  6187  caofid2  6188  mapen  6943  fival  7072  supelti  7104  supmaxti  7106  infminti  7129  xnegdi  9990  frecuzrdgsuc  10559  hashunlem  10949  ccatrn  11065  swrdccat2  11124  2zsupmax  11537  xrmin1inf  11578  serf0  11663  fsumabs  11776  binomlem  11794  cvgratz  11843  efcllemp  11969  ef0lem  11971  tannegap  12039  modm1div  12111  divalglemnqt  12231  bitsfzolem  12265  lcmid  12402  hashdvds  12543  prmdivdiv  12559  odzcllem  12565  reumodprminv  12576  nnnn0modprm0  12578  pythagtrip  12606  pcmpt  12666  pockthg  12680  4sqlem9  12709  4sqleminfi  12720  4sqexercise1  12721  4sqlem11  12724  ennnfonelemkh  12783  ctinf  12801  nninfdclemcl  12819  nninfdclemp1  12821  setsslid  12883  imasival  13138  imasaddflemg  13148  grpinvalem  13217  issubmnd  13274  imasmnd  13285  isgrpinv  13386  grpinvssd  13409  pwssub  13445  imasgrp  13447  mulgnndir  13487  subginv  13517  subginvcl  13519  ghmpreima  13602  conjnsg  13617  srgidmlem  13740  ringidmlem  13784  imasring  13826  dvdsr01  13866  unitnegcl  13892  01eq0ring  13951  issubrng2  13972  subrginv  13999  subrgunit  14001  aprsym  14046  lmodvneg1  14092  lspsn  14178  isridlrng  14244  lidl0cl  14245  rspcl  14253  rspssid  14254  rnglidlmmgm  14258  2idlcpblrng  14285  quscrng  14295  rspsn  14296  znidom  14419  psrlinv  14446  psr1clfi  14450  topbas  14539  tgrest  14641  txss12  14738  mpomulcn  15038  cnplimclemle  15140  dvconstss  15170  efltlemlt  15246  coseq0q4123  15306  lgsval  15481  lgscllem  15484  gausslemma2dlem1a  15535  lgseisen  15551  lgsquadlem1  15554  lgsquadlem2  15555  2lgslem3a1  15574  2lgslem3b1  15575  2lgslem3c1  15576  2lgslem3d1  15577  2lgsoddprm  15590  neapmkvlem  16006