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  4515  caofid0l  6166  caofid0r  6167  caofid1  6168  caofid2  6169  mapen  6916  fival  7045  supelti  7077  supmaxti  7079  infminti  7102  xnegdi  9960  frecuzrdgsuc  10523  hashunlem  10913  2zsupmax  11408  xrmin1inf  11449  serf0  11534  fsumabs  11647  binomlem  11665  cvgratz  11714  efcllemp  11840  ef0lem  11842  tannegap  11910  modm1div  11982  divalglemnqt  12102  bitsfzolem  12136  lcmid  12273  hashdvds  12414  prmdivdiv  12430  odzcllem  12436  reumodprminv  12447  nnnn0modprm0  12449  pythagtrip  12477  pcmpt  12537  pockthg  12551  4sqlem9  12580  4sqleminfi  12591  4sqexercise1  12592  4sqlem11  12595  ennnfonelemkh  12654  ctinf  12672  nninfdclemcl  12690  nninfdclemp1  12692  setsslid  12754  imasival  13008  imasaddflemg  13018  grpinvalem  13087  issubmnd  13144  imasmnd  13155  isgrpinv  13256  grpinvssd  13279  pwssub  13315  imasgrp  13317  mulgnndir  13357  subginv  13387  subginvcl  13389  ghmpreima  13472  conjnsg  13487  srgidmlem  13610  ringidmlem  13654  imasring  13696  dvdsr01  13736  unitnegcl  13762  01eq0ring  13821  issubrng2  13842  subrginv  13869  subrgunit  13871  aprsym  13916  lmodvneg1  13962  lspsn  14048  isridlrng  14114  lidl0cl  14115  rspcl  14123  rspssid  14124  rnglidlmmgm  14128  2idlcpblrng  14155  quscrng  14165  rspsn  14166  znidom  14289  psrlinv  14312  psr1clfi  14316  topbas  14387  tgrest  14489  txss12  14586  mpomulcn  14886  cnplimclemle  14988  dvconstss  15018  efltlemlt  15094  coseq0q4123  15154  lgsval  15329  lgscllem  15332  gausslemma2dlem1a  15383  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425  2lgsoddprm  15438  neapmkvlem  15798