Theorem ad3antrrr 492

Description: Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad3antrrr	|- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )

Proof of Theorem ad3antrrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 276	. 2 |- ( ( ph /\ ch ) -> ps )
3	2	ad2antrr 488	1 |- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )

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 is referenced by:  ad4antr  494  ad5ant12  518  disjiun  4109  tfr1onlemaccex  6592  tfrcllemaccex  6605  phplem4on  7135  dif1enen  7150  elssdc  7175  en2eqpr  7180  unsnfidcex  7193  unsnfidcel  7194  unfidisj  7195  undifdc  7197  fiintim  7204  ssfirab  7210  suplub2ti  7305  djudom  7397  omp1eomlem  7398  difinfsnlem  7403  difinfinf  7405  ctssdclemn0  7414  ctssdc  7417  nnnninfeq2  7433  nninfisol  7437  nninfwlpoimlemginf  7480  cc3  7598  ltaddpr  7928  ltexprlemrl  7941  addcanprleml  7945  addcanprlemu  7946  aptiprleml  7970  aptiprlemu  7971  cauappcvgprlemdisj  7982  cauappcvgprlemladdrl  7988  caucvgprlemloc  8006  caucvgprlemladdrl  8009  caucvgprprlemopl  8028  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  suplocexprlemrl  8048  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  caucvgsrlemoffres  8131  suplocsrlem  8139  axcaucvglemcau  8229  axcaucvglemres  8230  negf1o  8672  apreim  8894  apsym  8897  apcotr  8898  apadd1  8899  apneg  8902  mulext1  8903  mulge0  8910  apti  8913  aprcl  8937  qapne  9989  xaddf  10196  xaddval  10197  zsupcllemstep  10611  qtri3or  10624  exbtwnzlemstep  10631  rebtwn2zlemstep  10636  addmodlteq  10784  seq3f1olemqsumk  10898  seq3f1oleml  10902  qsqeqor  11036  apexp1  11105  faclbnd  11128  hashennnuni  11167  swrdswrd  11422  swrdccatin1  11442  pfxccatin12lem3  11449  swrdccat3blem  11456  cvg1nlemres  11695  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemga  11733  minmax  11940  xrmaxleim  11954  xrmaxifle  11956  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxiflemcom  11959  xrmaxltsup  11968  xrmaxadd  11971  xrminmax  11975  xrbdtri  11986  climrecvg1n  12058  serf0  12062  zsumdc  12095  isumss  12102  fisumss  12103  fsum3cvg3  12107  fsumcl2lem  12109  fsumadd  12117  fsummulc2  12159  divcnv  12208  cvgratz  12243  mertenslem2  12247  zproddc  12290  fprodssdc  12301  fprodmul  12302  fprodsplitdc  12307  fprodcl2lem  12316  fprodle  12351  fprodmodd  12352  p1modz1  12505  dvds2ln  12535  divalglemeunn  12632  divalglemeuneg  12634  bitsfzolem  12665  dvdsbnd  12677  bezoutlemnewy  12717  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlembi  12726  dfgcd3  12731  uzwodc  12758  nninfctlemfo  12761  lcmgcdlem  12799  cncongr1  12825  cncongr2  12826  isprm5  12864  odzdvds  12968  pclemdc  13011  pceu  13018  dvdsprmpweqle  13060  pcadd  13063  1arith  13090  4sqexercise2  13122  4sqlem13m  13126  ballotfilemcdc  13167  ballotfilemsle  13192  ennnfonelemhom  13250  ennnfonelemrnh  13251  ctinfomlemom  13262  resmhm2b  13744  mhmid  13868  mhmmnd  13869  ghmgrp  13871  mulgfng  13877  conjnmzb  14033  imasabl  14089  gfsumval  14102  gfsumcl  14110  prdsval  14115  issrg  14208  ringinvnzdiv  14293  znunit  14933  psrval  14940  mplsubgfilemcl  14980  cnpnei  15210  cnntr  15216  cncnp  15221  lmtopcnp  15241  txdis1cn  15269  xmettxlem  15500  metcnp3  15502  fsumcncntop  15558  cncfco  15582  mulcncf  15599  dedekindeulemuub  15608  dedekindeulemlu  15612  dedekindicclemuub  15617  dedekindicclemlu  15621  dedekindicclemicc  15623  ivthinclemlr  15628  ivthinclemur  15630  limcimo  15656  cnplimcim  15658  plymullem1  15739  plycolemc  15749  plycj  15752  dvply2g  15757  pilem3  15774  lgsfcl2  16005  lgsval2lem  16009  lgsdir  16034  lgsne0  16037  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  lgsquad3  16083  umgrvad2edg  16332  usgredg2vlem2  16344  wlkvtxiedg  16466  wlkvtxiedgg  16467  clwwlkccatlem  16521  eupth2lem3lem4fi  16594  eupth2lemsfi  16599  peano4nninf  16910  nnnninfex  16926  trilpolemeq1  16950  trimul0or  16971