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  4525  caofid0l  6184  caofid0r  6185  caofid1  6186  caofid2  6187  mapen  6942  fival  7071  supelti  7103  supmaxti  7105  infminti  7128  xnegdi  9989  frecuzrdgsuc  10557  hashunlem  10947  ccatrn  11063  2zsupmax  11508  xrmin1inf  11549  serf0  11634  fsumabs  11747  binomlem  11765  cvgratz  11814  efcllemp  11940  ef0lem  11942  tannegap  12010  modm1div  12082  divalglemnqt  12202  bitsfzolem  12236  lcmid  12373  hashdvds  12514  prmdivdiv  12530  odzcllem  12536  reumodprminv  12547  nnnn0modprm0  12549  pythagtrip  12577  pcmpt  12637  pockthg  12651  4sqlem9  12680  4sqleminfi  12691  4sqexercise1  12692  4sqlem11  12695  ennnfonelemkh  12754  ctinf  12772  nninfdclemcl  12790  nninfdclemp1  12792  setsslid  12854  imasival  13109  imasaddflemg  13119  grpinvalem  13188  issubmnd  13245  imasmnd  13256  isgrpinv  13357  grpinvssd  13380  pwssub  13416  imasgrp  13418  mulgnndir  13458  subginv  13488  subginvcl  13490  ghmpreima  13573  conjnsg  13588  srgidmlem  13711  ringidmlem  13755  imasring  13797  dvdsr01  13837  unitnegcl  13863  01eq0ring  13922  issubrng2  13943  subrginv  13970  subrgunit  13972  aprsym  14017  lmodvneg1  14063  lspsn  14149  isridlrng  14215  lidl0cl  14216  rspcl  14224  rspssid  14225  rnglidlmmgm  14229  2idlcpblrng  14256  quscrng  14266  rspsn  14267  znidom  14390  psrlinv  14417  psr1clfi  14421  topbas  14510  tgrest  14612  txss12  14709  mpomulcn  15009  cnplimclemle  15111  dvconstss  15141  efltlemlt  15217  coseq0q4123  15277  lgsval  15452  lgscllem  15455  gausslemma2dlem1a  15506  lgseisen  15522  lgsquadlem1  15525  lgsquadlem2  15526  2lgslem3a1  15545  2lgslem3b1  15546  2lgslem3c1  15547  2lgslem3d1  15548  2lgsoddprm  15561  neapmkvlem  15968