Theorem syl2an2r 876

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

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  disjxiun  4649  brcogw  5290  ordtr3OLD  5770  funfni  5991  fvelimab  6253  dff3  6372  f1cofveqaeq  6515  grprinvlem  6872  boxcutc  7951  supmax  8373  cantnff  8571  infxpenlem  8836  cfsmolem  9092  tsken  9576  addmodlteq  12745  hashdifpr  13203  ccatalpha  13375  dvdsprmpweqle  15590  sylow1lem2  18014  lbsextlem2  19159  psrlinv  19397  mplsubglem  19434  mpllsslem  19435  evlslem1  19515  topbas  20776  clmvz  22911  gausslemma2dlem1a  25090  2lgslem3a1  25125  2lgslem3b1  25126  2lgslem3c1  25127  2lgslem3d1  25128  2lgsoddprm  25141  uhgrspansubgrlem  26182  usgrres  26200  usgrnbcnvfv  26267  finsumvtxdg2sstep  26445  uspgr2wlkeq  26542  redwlk  26569  pthdivtx  26625  usgr2wlkspthlem2  26654  2wlkdlem6  26827  umgr2wlkon  26846  rusgrnumwwlk  26870  clwwlksnscsh  26940  1wlkdlem2  26998  fusgreghash2wsp  27202  numclwwlk6  27248  ofpreima2  29466  eulerpartlemgvv  30438  nosupbnd1lem4  31857  scutbdaylt  31922  gneispace  38432  ax6e2ndeqALT  39167  sineq0ALT  39173  setsv  41348  lighneal  41528  sprsymrelfolem2  41743