Theorem syl2an2r 603

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 584	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  4620  caofid0l  6319  caofid0r  6320  caofid1  6321  caofid2  6322  mapen  7136  fidcen  7193  fival  7294  supelti  7332  supmaxti  7334  infminti  7357  xnegdi  10249  fzsplit3  10436  frecuzrdgsuc  10829  hashunlem  11222  ccatrn  11355  ccatalpha  11359  swrdccat2  11421  pfxsuff1eqwrdeq  11449  ccatpfx  11451  swrdccatin2  11479  pfxccatin12lem2  11481  2zsupmax  11970  xrmin1inf  12011  serf0  12096  fsumabs  12210  binomlem  12228  cvgratz  12277  efcllemp  12403  ef0lem  12405  tannegap  12473  modm1div  12545  divalglemnqt  12665  bitsfzolem  12699  lcmid  12836  hashdvds  12977  prmdivdiv  12993  odzcllem  12999  reumodprminv  13010  nnnn0modprm0  13012  pythagtrip  13040  pcmpt  13100  pockthg  13114  4sqlem9  13143  4sqleminfi  13154  4sqexercise1  13155  4sqlem11  13158  ballotfilemic  13228  ballotfilemrv2  13243  ennnfonelemkh  13281  ctinf  13299  nninfdclemcl  13317  nninfdclemp1  13319  setsslid  13381  imasival  13604  imasaddflemg  13614  grpinvalem  13682  issubmnd  13732  imasmnd  13737  isgrpinv  13836  grpinvssd  13859  imasgrp  13891  mulgnndir  13931  subginv  13961  subginvcl  13963  ghmpreima  14046  conjnsg  14061  gzsumsplit0  14125  gsumconstcmn  14143  pwssub  14193  srgidmlem  14256  ringidmlem  14300  imasring  14342  dvdsr01  14384  unitnegcl  14410  01eq0ring  14469  issubrng2  14491  subrginv  14518  subrgunit  14520  aprsym  14569  lmodvneg1  14639  lspsn  14725  isridlrng  14791  lidl0cl  14792  rspcl  14800  rspssid  14801  rnglidlmmgm  14805  2idlcpblrng  14832  quscrng  14842  rspsn  14843  znidom  14964  psrlinv  14998  psr1clfi  15002  topbas  15091  tgrest  15193  txss12  15290  mpomulcn  15590  cnplimclemle  15692  dvconstss  15722  efltlemlt  15798  coseq0q4123  15858  lgsval  16037  lgscllem  16040  gausslemma2dlem1a  16091  lgseisen  16107  lgsquadlem1  16110  lgsquadlem2  16111  2lgslem3a1  16130  2lgslem3b1  16131  2lgslem3c1  16132  2lgslem3d1  16133  2lgsoddprm  16146  uhgrspansubgrlem  16431  uspgr2wlkeq  16520  neapmkvlem  17022