Theorem syl2an2r 562

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  op1stbg  4299  mapen  6552  supelti  6687  supmaxti  6689  infminti  6712  frecuzrdgsuc  9809  hashunlem  10200  serf0  10728  fsumabs  10846  binomlem  10864  cvgratz  10913  efcllemp  10935  ef0lem  10937  tannegap  11006  divalglemnqt  11185  lcmid  11327  hashdvds  11462