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  4539  caofid0l  6203  caofid0r  6204  caofid1  6205  caofid2  6206  mapen  6963  fival  7093  supelti  7125  supmaxti  7127  infminti  7150  xnegdi  10020  frecuzrdgsuc  10591  hashunlem  10981  ccatrn  11098  swrdccat2  11157  pfxsuff1eqwrdeq  11185  ccatpfx  11187  2zsupmax  11622  xrmin1inf  11663  serf0  11748  fsumabs  11861  binomlem  11879  cvgratz  11928  efcllemp  12054  ef0lem  12056  tannegap  12124  modm1div  12196  divalglemnqt  12316  bitsfzolem  12350  lcmid  12487  hashdvds  12628  prmdivdiv  12644  odzcllem  12650  reumodprminv  12661  nnnn0modprm0  12663  pythagtrip  12691  pcmpt  12751  pockthg  12765  4sqlem9  12794  4sqleminfi  12805  4sqexercise1  12806  4sqlem11  12809  ennnfonelemkh  12868  ctinf  12886  nninfdclemcl  12904  nninfdclemp1  12906  setsslid  12968  imasival  13223  imasaddflemg  13233  grpinvalem  13302  issubmnd  13359  imasmnd  13370  isgrpinv  13471  grpinvssd  13494  pwssub  13530  imasgrp  13532  mulgnndir  13572  subginv  13602  subginvcl  13604  ghmpreima  13687  conjnsg  13702  srgidmlem  13825  ringidmlem  13869  imasring  13911  dvdsr01  13951  unitnegcl  13977  01eq0ring  14036  issubrng2  14057  subrginv  14084  subrgunit  14086  aprsym  14131  lmodvneg1  14177  lspsn  14263  isridlrng  14329  lidl0cl  14330  rspcl  14338  rspssid  14339  rnglidlmmgm  14343  2idlcpblrng  14370  quscrng  14380  rspsn  14381  znidom  14504  psrlinv  14531  psr1clfi  14535  topbas  14624  tgrest  14726  txss12  14823  mpomulcn  15123  cnplimclemle  15225  dvconstss  15255  efltlemlt  15331  coseq0q4123  15391  lgsval  15566  lgscllem  15569  gausslemma2dlem1a  15620  lgseisen  15636  lgsquadlem1  15639  lgsquadlem2  15640  2lgslem3a1  15659  2lgslem3b1  15660  2lgslem3c1  15661  2lgslem3d1  15662  2lgsoddprm  15675  neapmkvlem  16178