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  4625  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  mapen  7146  fidcen  7203  fival  7304  supelti  7342  supmaxti  7344  infminti  7367  xnegdi  10280  fzsplit3  10468  frecuzrdgsuc  10864  nn0sqdc  11160  hashunlem  11258  ccatrn  11391  ccatalpha  11395  swrdccat2  11457  pfxsuff1eqwrdeq  11485  ccatpfx  11487  swrdccatin2  11515  pfxccatin12lem2  11517  2zsupmax  12007  xrmin1inf  12049  serf0  12134  fsumabs  12248  binomlem  12266  cvgratz  12315  efcllemp  12441  ef0lem  12443  tannegap  12511  modm1div  12583  divalglemnqt  12703  bitsfzolem  12737  lcmid  12874  pwbdvdseulemle  12962  hashdvds  13019  prmdivdiv  13035  odzcllem  13041  reumodprminv  13052  nnnn0modprm0  13054  pythagtrip  13082  pcmpt  13142  pockthg  13156  4sqlem9  13185  4sqleminfi  13196  4sqexercise1  13197  4sqlem11  13200  ballotfilemic  13299  ballotfilemrv2  13314  ennnfonelemkh  13352  ctinf  13370  nninfdclemcl  13388  nninfdclemp1  13390  setsslid  13452  imasival  13676  imasaddflemg  13686  grpinvalem  13754  issubmnd  13804  imasmnd  13809  isgrpinv  13908  grpinvssd  13931  imasgrp  13963  mulgnndir  14003  subginv  14033  subginvcl  14035  ghmpreima  14118  conjnsg  14133  gzsumsplit0  14197  gsumconstcmn  14215  pwssub  14265  srgidmlem  14331  ringidmlem  14376  imasring  14418  dvdsr01  14460  unitnegcl  14486  01eq0ring  14545  issubrng2  14567  subrginv  14594  subrgunit  14596  aprsym  14645  lmodvneg1  14716  lspsn  14802  isridlrng  14868  lidl0cl  14869  rspcl  14877  rspssid  14878  rnglidlmmgm  14882  2idlcpblrng  14909  quscrng  14919  rspsn  14920  znidom  15041  psrlinv  15124  psr1clfi  15128  topbas  15217  tgrest  15319  txss12  15416  mpomulcn  15716  cnplimclemle  15818  dvconstss  15848  efltlemlt  15924  coseq0q4123  15985  bposlem2  16210  lgsval  16221  lgscllem  16224  gausslemma2dlem1a  16275  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  2lgslem3a1  16314  2lgslem3b1  16315  2lgslem3c1  16316  2lgslem3d1  16317  2lgsoddprm  16330  uhgrspansubgrlem  16615  uspgr2wlkeq  16704  neapmkvlem  17215