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  4511  mapen  6904  fival  7031  supelti  7063  supmaxti  7065  infminti  7088  xnegdi  9937  frecuzrdgsuc  10488  hashunlem  10878  2zsupmax  11372  xrmin1inf  11413  serf0  11498  fsumabs  11611  binomlem  11629  cvgratz  11678  efcllemp  11804  ef0lem  11806  tannegap  11874  modm1div  11946  divalglemnqt  12064  lcmid  12221  hashdvds  12362  prmdivdiv  12378  odzcllem  12383  reumodprminv  12394  nnnn0modprm0  12396  pythagtrip  12424  pcmpt  12484  pockthg  12498  4sqlem9  12527  4sqleminfi  12538  4sqexercise1  12539  4sqlem11  12542  ennnfonelemkh  12572  ctinf  12590  nninfdclemcl  12608  nninfdclemp1  12610  setsslid  12672  imasival  12892  imasaddflemg  12902  grpinvalem  12971  issubmnd  13026  isgrpinv  13129  grpinvssd  13152  imasgrp  13184  mulgnndir  13224  subginv  13254  subginvcl  13256  ghmpreima  13339  conjnsg  13354  srgidmlem  13477  ringidmlem  13521  imasring  13563  dvdsr01  13603  unitnegcl  13629  01eq0ring  13688  issubrng2  13709  subrginv  13736  subrgunit  13738  aprsym  13783  lmodvneg1  13829  lspsn  13915  isridlrng  13981  lidl0cl  13982  rspcl  13990  rspssid  13991  rnglidlmmgm  13995  2idlcpblrng  14022  quscrng  14032  rspsn  14033  znidom  14156  topbas  14246  tgrest  14348  txss12  14445  mpomulcn  14745  cnplimclemle  14847  dvconstss  14877  efltlemlt  14950  coseq0q4123  15010  lgsval  15161  lgscllem  15164  gausslemma2dlem1a  15215  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgslem3d1  15257  2lgsoddprm  15270  neapmkvlem  15627