Theorem syl2an2r 585

Description: syl2anr 288 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 287	. 2 |- ( ( ph /\ ( ph /\ ch ) ) -> ta )
5	4	anabss5 568	1 |- ( ( ph /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  op1stbg  4456  mapen  6808  fival  6931  supelti  6963  supmaxti  6965  infminti  6988  xnegdi  9800  frecuzrdgsuc  10345  hashunlem  10713  2zsupmax  11163  xrmin1inf  11204  serf0  11289  fsumabs  11402  binomlem  11420  cvgratz  11469  efcllemp  11595  ef0lem  11597  tannegap  11665  modm1div  11736  divalglemnqt  11853  lcmid  12008  hashdvds  12149  prmdivdiv  12165  odzcllem  12170  reumodprminv  12181  nnnn0modprm0  12183  pythagtrip  12211  pcmpt  12269  pockthg  12283  4sqlem9  12312  ennnfonelemkh  12341  ctinf  12359  nninfdclemp1  12379  setsslid  12440  topbas  12667  tgrest  12769  txss12  12866  cnplimclemle  13237  efltlemlt  13295  coseq0q4123  13355  lgsval  13505  lgscllem  13508  neapmkvlem  13905