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  7343  supmaxti  7345  infminti  7368  xnegdi  10281  fzsplit3  10469  frecuzrdgsuc  10865  nn0sqdc  11161  hashunlem  11259  ccatrn  11392  ccatalpha  11396  swrdccat2  11458  pfxsuff1eqwrdeq  11486  ccatpfx  11488  swrdccatin2  11516  pfxccatin12lem2  11518  2zsupmax  12008  xrmin1inf  12051  serf0  12136  fsumabs  12250  binomlem  12268  cvgratz  12317  efcllemp  12443  ef0lem  12445  tannegap  12513  modm1div  12585  divalglemnqt  12705  bitsfzolem  12739  lcmid  12876  pwbdvdseulemle  12964  hashdvds  13021  prmdivdiv  13037  odzcllem  13043  reumodprminv  13054  nnnn0modprm0  13056  pythagtrip  13084  pcmpt  13144  pockthg  13158  4sqlem9  13187  4sqleminfi  13198  4sqexercise1  13199  4sqlem11  13202  ballotfilemic  13301  ballotfilemrv2  13316  ennnfonelemkh  13354  ctinf  13372  nninfdclemcl  13390  nninfdclemp1  13392  setsslid  13454  imasival  13678  imasaddflemg  13688  grpinvalem  13756  issubmnd  13806  imasmnd  13811  isgrpinv  13910  grpinvssd  13933  imasgrp  13965  mulgnndir  14005  subginv  14035  subginvcl  14037  ghmpreima  14120  conjnsg  14135  gzsumsplit0  14199  gsumconstcmn  14217  pwssub  14267  srgidmlem  14333  ringidmlem  14378  imasring  14420  dvdsr01  14462  unitnegcl  14488  01eq0ring  14547  issubrng2  14569  subrginv  14596  subrgunit  14598  aprsym  14647  lmodvneg1  14718  lspsn  14804  isridlrng  14870  lidl0cl  14871  rspcl  14879  rspssid  14880  rnglidlmmgm  14884  2idlcpblrng  14911  quscrng  14921  rspsn  14922  znidom  15043  psrlinv  15127  psr1clfi  15131  topbas  15220  tgrest  15322  txss12  15419  mpomulcn  15719  cnplimclemle  15821  dvconstss  15851  efltlemlt  15927  coseq0q4123  15988  chtqub  16218  bposlem2  16234  lgsval  16245  lgscllem  16248  gausslemma2dlem1a  16299  lgseisen  16315  lgsquadlem1  16318  lgsquadlem2  16319  2lgslem3a1  16338  2lgslem3b1  16339  2lgslem3c1  16340  2lgslem3d1  16341  2lgsoddprm  16354  uhgrspansubgrlem  16639  uspgr2wlkeq  16728  neapmkvlem  17239