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  4510  mapen  6902  fival  7029  supelti  7061  supmaxti  7063  infminti  7086  xnegdi  9934  frecuzrdgsuc  10485  hashunlem  10875  2zsupmax  11369  xrmin1inf  11410  serf0  11495  fsumabs  11608  binomlem  11626  cvgratz  11675  efcllemp  11801  ef0lem  11803  tannegap  11871  modm1div  11943  divalglemnqt  12061  lcmid  12218  hashdvds  12359  prmdivdiv  12375  odzcllem  12380  reumodprminv  12391  nnnn0modprm0  12393  pythagtrip  12421  pcmpt  12481  pockthg  12495  4sqlem9  12524  4sqleminfi  12535  4sqexercise1  12536  4sqlem11  12539  ennnfonelemkh  12569  ctinf  12587  nninfdclemcl  12605  nninfdclemp1  12607  setsslid  12669  imasival  12889  imasaddflemg  12899  grpinvalem  12968  issubmnd  13023  isgrpinv  13126  grpinvssd  13149  imasgrp  13181  mulgnndir  13221  subginv  13251  subginvcl  13253  ghmpreima  13336  conjnsg  13351  srgidmlem  13474  ringidmlem  13518  imasring  13560  dvdsr01  13600  unitnegcl  13626  01eq0ring  13685  issubrng2  13706  subrginv  13733  subrgunit  13735  aprsym  13780  lmodvneg1  13826  lspsn  13912  isridlrng  13978  lidl0cl  13979  rspcl  13987  rspssid  13988  rnglidlmmgm  13992  2idlcpblrng  14019  quscrng  14029  rspsn  14030  znidom  14145  topbas  14235  tgrest  14337  txss12  14434  cnplimclemle  14822  efltlemlt  14909  coseq0q4123  14969  lgsval  15120  lgscllem  15123  gausslemma2dlem1a  15174  lgseisen  15190  lgsquadlem1  15191  neapmkvlem  15557