Theorem syl2an2r 584

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 567	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  4400  mapen  6740  fival  6858  supelti  6889  supmaxti  6891  infminti  6914  xnegdi  9651  frecuzrdgsuc  10187  hashunlem  10550  2zsupmax  10997  xrmin1inf  11036  serf0  11121  fsumabs  11234  binomlem  11252  cvgratz  11301  efcllemp  11364  ef0lem  11366  tannegap  11435  divalglemnqt  11617  lcmid  11761  hashdvds  11897  ennnfonelemkh  11925  ctinf  11943  setsslid  12009  topbas  12236  tgrest  12338  txss12  12435  cnplimclemle  12806  coseq0q4123  12915