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  10270  fzsplit3  10458  frecuzrdgsuc  10851  hashunlem  11244  ccatrn  11377  ccatalpha  11381  swrdccat2  11443  pfxsuff1eqwrdeq  11471  ccatpfx  11473  swrdccatin2  11501  pfxccatin12lem2  11503  2zsupmax  11992  xrmin1inf  12033  serf0  12118  fsumabs  12232  binomlem  12250  cvgratz  12299  efcllemp  12425  ef0lem  12427  tannegap  12495  modm1div  12567  divalglemnqt  12687  bitsfzolem  12721  lcmid  12858  hashdvds  12999  prmdivdiv  13015  odzcllem  13021  reumodprminv  13032  nnnn0modprm0  13034  pythagtrip  13062  pcmpt  13122  pockthg  13136  4sqlem9  13165  4sqleminfi  13176  4sqexercise1  13177  4sqlem11  13180  ballotfilemic  13250  ballotfilemrv2  13265  ennnfonelemkh  13303  ctinf  13321  nninfdclemcl  13339  nninfdclemp1  13341  setsslid  13403  imasival  13627  imasaddflemg  13637  grpinvalem  13705  issubmnd  13755  imasmnd  13760  isgrpinv  13859  grpinvssd  13882  imasgrp  13914  mulgnndir  13954  subginv  13984  subginvcl  13986  ghmpreima  14069  conjnsg  14084  gzsumsplit0  14148  gsumconstcmn  14166  pwssub  14216  srgidmlem  14282  ringidmlem  14327  imasring  14369  dvdsr01  14411  unitnegcl  14437  01eq0ring  14496  issubrng2  14518  subrginv  14545  subrgunit  14547  aprsym  14596  lmodvneg1  14667  lspsn  14753  isridlrng  14819  lidl0cl  14820  rspcl  14828  rspssid  14829  rnglidlmmgm  14833  2idlcpblrng  14860  quscrng  14870  rspsn  14871  znidom  14992  psrlinv  15075  psr1clfi  15079  topbas  15168  tgrest  15270  txss12  15367  mpomulcn  15667  cnplimclemle  15769  dvconstss  15799  efltlemlt  15875  coseq0q4123  15935  lgsval  16123  lgscllem  16126  gausslemma2dlem1a  16177  lgseisen  16193  lgsquadlem1  16196  lgsquadlem2  16197  2lgslem3a1  16216  2lgslem3b1  16217  2lgslem3c1  16218  2lgslem3d1  16219  2lgsoddprm  16232  uhgrspansubgrlem  16517  uspgr2wlkeq  16606  neapmkvlem  17117