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  4493  mapen  6863  fival  6986  supelti  7018  supmaxti  7020  infminti  7043  xnegdi  9885  frecuzrdgsuc  10431  hashunlem  10801  2zsupmax  11251  xrmin1inf  11292  serf0  11377  fsumabs  11490  binomlem  11508  cvgratz  11557  efcllemp  11683  ef0lem  11685  tannegap  11753  modm1div  11824  divalglemnqt  11942  lcmid  12097  hashdvds  12238  prmdivdiv  12254  odzcllem  12259  reumodprminv  12270  nnnn0modprm0  12272  pythagtrip  12300  pcmpt  12358  pockthg  12372  4sqlem9  12401  ennnfonelemkh  12430  ctinf  12448  nninfdclemp1  12468  setsslid  12530  imasival  12748  imasaddflemg  12758  grpinvalem  12826  issubmnd  12868  isgrpinv  12963  grpinvssd  12986  imasgrp  13018  mulgnndir  13056  subginv  13085  subginvcl  13087  ghmpreima  13165  conjnsg  13180  srgidmlem  13292  ringidmlem  13336  imasring  13374  dvdsr01  13414  unitnegcl  13440  01eq0ring  13496  issubrng2  13517  subrginv  13544  subrgunit  13546  aprsym  13560  lmodvneg1  13606  lspsn  13692  isridlrng  13758  lidl0cl  13759  rspcl  13767  rspssid  13768  rnglidlmmgm  13772  2idlcpblrng  13798  quscrng  13807  topbas  13950  tgrest  14052  txss12  14149  cnplimclemle  14520  efltlemlt  14578  coseq0q4123  14638  lgsval  14788  lgscllem  14791  neapmkvlem  15199