Theorem syl2an2r 597

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  4570  caofid0l  6251  caofid0r  6252  caofid1  6253  caofid2  6254  mapen  7015  fidcen  7069  fival  7148  supelti  7180  supmaxti  7182  infminti  7205  xnegdi  10076  frecuzrdgsuc  10648  hashunlem  11038  ccatrn  11157  ccatalpha  11161  swrdccat2  11218  pfxsuff1eqwrdeq  11246  ccatpfx  11248  swrdccatin2  11276  pfxccatin12lem2  11278  2zsupmax  11752  xrmin1inf  11793  serf0  11878  fsumabs  11991  binomlem  12009  cvgratz  12058  efcllemp  12184  ef0lem  12186  tannegap  12254  modm1div  12326  divalglemnqt  12446  bitsfzolem  12480  lcmid  12617  hashdvds  12758  prmdivdiv  12774  odzcllem  12780  reumodprminv  12791  nnnn0modprm0  12793  pythagtrip  12821  pcmpt  12881  pockthg  12895  4sqlem9  12924  4sqleminfi  12935  4sqexercise1  12936  4sqlem11  12939  ennnfonelemkh  12998  ctinf  13016  nninfdclemcl  13034  nninfdclemp1  13036  setsslid  13098  imasival  13354  imasaddflemg  13364  grpinvalem  13433  issubmnd  13490  imasmnd  13501  isgrpinv  13602  grpinvssd  13625  pwssub  13661  imasgrp  13663  mulgnndir  13703  subginv  13733  subginvcl  13735  ghmpreima  13818  conjnsg  13833  srgidmlem  13956  ringidmlem  14000  imasring  14042  dvdsr01  14083  unitnegcl  14109  01eq0ring  14168  issubrng2  14189  subrginv  14216  subrgunit  14218  aprsym  14263  lmodvneg1  14309  lspsn  14395  isridlrng  14461  lidl0cl  14462  rspcl  14470  rspssid  14471  rnglidlmmgm  14475  2idlcpblrng  14502  quscrng  14512  rspsn  14513  znidom  14636  psrlinv  14663  psr1clfi  14667  topbas  14756  tgrest  14858  txss12  14955  mpomulcn  15255  cnplimclemle  15357  dvconstss  15387  efltlemlt  15463  coseq0q4123  15523  lgsval  15698  lgscllem  15701  gausslemma2dlem1a  15752  lgseisen  15768  lgsquadlem1  15771  lgsquadlem2  15772  2lgslem3a1  15791  2lgslem3b1  15792  2lgslem3c1  15793  2lgslem3d1  15794  2lgsoddprm  15807  uspgr2wlkeq  16106  neapmkvlem  16495