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  4046  tfr1onlemaccex  6447  tfrcllemaccex  6460  phplem4on  6979  dif1enen  6992  en2eqpr  7019  unsnfidcex  7032  unsnfidcel  7033  unfidisj  7034  undifdc  7036  fiintim  7043  ssfirab  7048  suplub2ti  7118  djudom  7210  omp1eomlem  7211  difinfsnlem  7216  difinfinf  7218  ctssdclemn0  7227  ctssdc  7230  nnnninfeq2  7246  nninfisol  7250  nninfwlpoimlemginf  7293  cc3  7400  ltaddpr  7730  ltexprlemrl  7743  addcanprleml  7747  addcanprlemu  7748  aptiprleml  7772  aptiprlemu  7773  cauappcvgprlemdisj  7784  cauappcvgprlemladdrl  7790  caucvgprlemloc  7808  caucvgprlemladdrl  7811  caucvgprprlemopl  7830  caucvgprprlemloc  7836  caucvgprprlemexbt  7839  suplocexprlemrl  7850  suplocexprlemru  7852  suplocexprlemdisj  7853  suplocexprlemloc  7854  suplocexprlemub  7856  caucvgsrlemoffres  7933  suplocsrlem  7941  axcaucvglemcau  8031  axcaucvglemres  8032  negf1o  8474  apreim  8696  apsym  8699  apcotr  8700  apadd1  8701  apneg  8704  mulext1  8705  mulge0  8712  apti  8715  aprcl  8739  qapne  9780  xaddf  9986  xaddval  9987  zsupcllemstep  10394  qtri3or  10405  exbtwnzlemstep  10412  rebtwn2zlemstep  10417  addmodlteq  10565  seq3f1olemqsumk  10679  seq3f1oleml  10683  qsqeqor  10817  apexp1  10885  faclbnd  10908  hashennnuni  10946  swrdswrd  11181  cvg1nlemres  11371  resqrexlemoverl  11407  resqrexlemglsq  11408  resqrexlemga  11409  minmax  11616  xrmaxleim  11630  xrmaxifle  11632  xrmaxiflemab  11633  xrmaxiflemlub  11634  xrmaxiflemcom  11635  xrmaxltsup  11644  xrmaxadd  11647  xrminmax  11651  xrbdtri  11662  climrecvg1n  11734  serf0  11738  zsumdc  11770  isumss  11777  fisumss  11778  fsum3cvg3  11782  fsumcl2lem  11784  fsumadd  11792  fsummulc2  11834  divcnv  11883  cvgratz  11918  mertenslem2  11922  zproddc  11965  fprodssdc  11976  fprodmul  11977  fprodsplitdc  11982  fprodcl2lem  11991  fprodle  12026  fprodmodd  12027  p1modz1  12180  dvds2ln  12210  divalglemeunn  12307  divalglemeuneg  12309  bitsfzolem  12340  dvdsbnd  12352  bezoutlemnewy  12392  bezoutlemstep  12393  bezoutlemmain  12394  bezoutlembi  12401  dfgcd3  12406  uzwodc  12433  nninfctlemfo  12436  lcmgcdlem  12474  cncongr1  12500  cncongr2  12501  isprm5  12539  odzdvds  12643  pclemdc  12686  pceu  12693  dvdsprmpweqle  12735  pcadd  12738  1arith  12765  4sqexercise2  12797  4sqlem13m  12801  ennnfonelemhom  12861  ennnfonelemrnh  12862  ctinfomlemom  12873  prdsval  13180  resmhm2b  13396  mhmid  13526  mhmmnd  13527  ghmgrp  13529  mulgfng  13535  conjnmzb  13691  imasabl  13747  issrg  13802  ringinvnzdiv  13887  znunit  14496  psrval  14503  mplsubgfilemcl  14536  cnpnei  14766  cnntr  14772  cncnp  14777  lmtopcnp  14797  txdis1cn  14825  xmettxlem  15056  metcnp3  15058  fsumcncntop  15114  cncfco  15138  mulcncf  15155  dedekindeulemuub  15164  dedekindeulemlu  15168  dedekindicclemuub  15173  dedekindicclemlu  15177  dedekindicclemicc  15179  ivthinclemlr  15184  ivthinclemur  15186  limcimo  15212  cnplimcim  15214  plymullem1  15295  plycolemc  15305  plycj  15308  dvply2g  15313  pilem3  15330  lgsfcl2  15558  lgsval2lem  15562  lgsdir  15587  lgsne0  15590  gausslemma2dlem1a  15610  gausslemma2dlem1f1o  15612  lgsquad3  15636  peano4nninf  16084  nnnninfex  16100  trilpolemeq1  16120