Theorem syl2an2r 599

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 580	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  4576  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  mapen  7032  fidcen  7088  fival  7169  supelti  7201  supmaxti  7203  infminti  7226  xnegdi  10103  frecuzrdgsuc  10676  hashunlem  11067  ccatrn  11186  ccatalpha  11190  swrdccat2  11252  pfxsuff1eqwrdeq  11280  ccatpfx  11282  swrdccatin2  11310  pfxccatin12lem2  11312  2zsupmax  11787  xrmin1inf  11828  serf0  11913  fsumabs  12027  binomlem  12045  cvgratz  12094  efcllemp  12220  ef0lem  12222  tannegap  12290  modm1div  12362  divalglemnqt  12482  bitsfzolem  12516  lcmid  12653  hashdvds  12794  prmdivdiv  12810  odzcllem  12816  reumodprminv  12827  nnnn0modprm0  12829  pythagtrip  12857  pcmpt  12917  pockthg  12931  4sqlem9  12960  4sqleminfi  12971  4sqexercise1  12972  4sqlem11  12975  ennnfonelemkh  13034  ctinf  13052  nninfdclemcl  13070  nninfdclemp1  13072  setsslid  13134  imasival  13390  imasaddflemg  13400  grpinvalem  13469  issubmnd  13526  imasmnd  13537  isgrpinv  13638  grpinvssd  13661  pwssub  13697  imasgrp  13699  mulgnndir  13739  subginv  13769  subginvcl  13771  ghmpreima  13854  conjnsg  13869  gsumsplit0  13934  srgidmlem  13993  ringidmlem  14037  imasring  14079  dvdsr01  14120  unitnegcl  14146  01eq0ring  14205  issubrng2  14226  subrginv  14253  subrgunit  14255  aprsym  14300  lmodvneg1  14346  lspsn  14432  isridlrng  14498  lidl0cl  14499  rspcl  14507  rspssid  14508  rnglidlmmgm  14512  2idlcpblrng  14539  quscrng  14549  rspsn  14550  znidom  14673  psrlinv  14700  psr1clfi  14704  topbas  14793  tgrest  14895  txss12  14992  mpomulcn  15292  cnplimclemle  15394  dvconstss  15424  efltlemlt  15500  coseq0q4123  15560  lgsval  15735  lgscllem  15738  gausslemma2dlem1a  15789  lgseisen  15805  lgsquadlem1  15808  lgsquadlem2  15809  2lgslem3a1  15828  2lgslem3b1  15829  2lgslem3c1  15830  2lgslem3d1  15831  2lgsoddprm  15844  uhgrspansubgrlem  16129  uspgr2wlkeq  16218  neapmkvlem  16674