Theorem syl2an2r 597

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  4574  caofid0l  6257  caofid0r  6258  caofid1  6259  caofid2  6260  mapen  7027  fidcen  7081  fival  7160  supelti  7192  supmaxti  7194  infminti  7217  xnegdi  10093  frecuzrdgsuc  10666  hashunlem  11057  ccatrn  11176  ccatalpha  11180  swrdccat2  11242  pfxsuff1eqwrdeq  11270  ccatpfx  11272  swrdccatin2  11300  pfxccatin12lem2  11302  2zsupmax  11777  xrmin1inf  11818  serf0  11903  fsumabs  12016  binomlem  12034  cvgratz  12083  efcllemp  12209  ef0lem  12211  tannegap  12279  modm1div  12351  divalglemnqt  12471  bitsfzolem  12505  lcmid  12642  hashdvds  12783  prmdivdiv  12799  odzcllem  12805  reumodprminv  12816  nnnn0modprm0  12818  pythagtrip  12846  pcmpt  12906  pockthg  12920  4sqlem9  12949  4sqleminfi  12960  4sqexercise1  12961  4sqlem11  12964  ennnfonelemkh  13023  ctinf  13041  nninfdclemcl  13059  nninfdclemp1  13061  setsslid  13123  imasival  13379  imasaddflemg  13389  grpinvalem  13458  issubmnd  13515  imasmnd  13526  isgrpinv  13627  grpinvssd  13650  pwssub  13686  imasgrp  13688  mulgnndir  13728  subginv  13758  subginvcl  13760  ghmpreima  13843  conjnsg  13858  srgidmlem  13981  ringidmlem  14025  imasring  14067  dvdsr01  14108  unitnegcl  14134  01eq0ring  14193  issubrng2  14214  subrginv  14241  subrgunit  14243  aprsym  14288  lmodvneg1  14334  lspsn  14420  isridlrng  14486  lidl0cl  14487  rspcl  14495  rspssid  14496  rnglidlmmgm  14500  2idlcpblrng  14527  quscrng  14537  rspsn  14538  znidom  14661  psrlinv  14688  psr1clfi  14692  topbas  14781  tgrest  14883  txss12  14980  mpomulcn  15280  cnplimclemle  15382  dvconstss  15412  efltlemlt  15488  coseq0q4123  15548  lgsval  15723  lgscllem  15726  gausslemma2dlem1a  15777  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  2lgslem3a1  15816  2lgslem3b1  15817  2lgslem3c1  15818  2lgslem3d1  15819  2lgsoddprm  15832  uspgr2wlkeq  16162  neapmkvlem  16607