Theorem syl2an2r 603

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 584	1 |- ( ( ph /\ ch ) -> ta )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  op1stbg  4627  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  mapen  7150  fidcen  7207  fival  7309  supelti  7348  supmaxti  7350  infminti  7373  xnegdi  10287  fzsplit3  10475  frecuzrdgsuc  10872  nn0sqdc  11168  hashunlem  11266  ccatrn  11399  ccatalpha  11403  swrdccat2  11465  pfxsuff1eqwrdeq  11493  ccatpfx  11495  swrdccatin2  11523  pfxccatin12lem2  11525  2zsupmax  12015  xrmin1inf  12058  serf0  12143  fsumabs  12257  binomlem  12275  cvgratz  12324  efcllemp  12450  ef0lem  12452  tannegap  12520  modm1div  12592  divalglemnqt  12712  bitsfzolem  12746  lcmid  12883  pwbdvdseulemle  12971  hashdvds  13028  prmdivdiv  13044  odzcllem  13050  reumodprminv  13061  nnnn0modprm0  13063  pythagtrip  13091  pcmpt  13151  pockthg  13165  4sqlem9  13194  4sqleminfi  13205  4sqexercise1  13206  4sqlem11  13209  ballotfilemic  13308  ballotfilemrv2  13323  ennnfonelemkh  13361  ctinf  13379  nninfdclemcl  13397  nninfdclemp1  13399  setsslid  13461  imasival  13686  imasaddflemg  13696  grpinvalem  13764  issubmnd  13814  imasmnd  13819  isgrpinv  13918  grpinvssd  13941  imasgrp  13973  mulgnndir  14013  subginv  14043  subginvcl  14045  ghmpreima  14128  conjnsg  14143  gzsumsplit0  14238  gsumconstcmn  14266  pwssub  14323  srgidmlem  14389  ringidmlem  14434  imasring  14478  dvdsr01  14520  unitnegcl  14546  01eq0ring  14605  issubrng2  14627  subrginv  14654  subrgunit  14656  aprsym  14705  lmodvneg1  14776  lspsn  14862  isridlrng  14928  lidl0cl  14929  rspcl  14937  rspssid  14938  rnglidlmmgm  14942  2idlcpblrng  14969  quscrng  14979  rspsn  14980  znidom  15101  psrlinv  15194  psr1clfi  15198  topbas  15293  tgrest  15395  txss12  15492  mpomulcn  15792  cnplimclemle  15894  dvconstss  15924  efltlemlt  16000  coseq0q4123  16061  chtqub  16296  bposlem2  16312  lgsval  16328  lgscllem  16331  gausslemma2dlem1a  16382  lgseisen  16398  lgsquadlem1  16401  lgsquadlem2  16402  2lgslem3a1  16421  2lgslem3b1  16422  2lgslem3c1  16423  2lgslem3d1  16424  2lgsoddprm  16437  uhgrspansubgrlem  16722  uspgr2wlkeq  16811  neapmkvlem  17324