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  4083  tfr1onlemaccex  6514  tfrcllemaccex  6527  phplem4on  7054  dif1enen  7069  elssdc  7094  en2eqpr  7099  unsnfidcex  7112  unsnfidcel  7113  unfidisj  7114  undifdc  7116  fiintim  7123  ssfirab  7129  suplub2ti  7200  djudom  7292  omp1eomlem  7293  difinfsnlem  7298  difinfinf  7300  ctssdclemn0  7309  ctssdc  7312  nnnninfeq2  7328  nninfisol  7332  nninfwlpoimlemginf  7375  cc3  7487  ltaddpr  7817  ltexprlemrl  7830  addcanprleml  7834  addcanprlemu  7835  aptiprleml  7859  aptiprlemu  7860  cauappcvgprlemdisj  7871  cauappcvgprlemladdrl  7877  caucvgprlemloc  7895  caucvgprlemladdrl  7898  caucvgprprlemopl  7917  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  suplocexprlemrl  7937  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  caucvgsrlemoffres  8020  suplocsrlem  8028  axcaucvglemcau  8118  axcaucvglemres  8119  negf1o  8561  apreim  8783  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  mulge0  8799  apti  8802  aprcl  8826  qapne  9873  xaddf  10079  xaddval  10080  zsupcllemstep  10490  qtri3or  10501  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  addmodlteq  10661  seq3f1olemqsumk  10775  seq3f1oleml  10779  qsqeqor  10913  apexp1  10981  faclbnd  11004  hashennnuni  11042  swrdswrd  11290  swrdccatin1  11310  pfxccatin12lem3  11317  swrdccat3blem  11324  cvg1nlemres  11563  resqrexlemoverl  11599  resqrexlemglsq  11600  resqrexlemga  11601  minmax  11808  xrmaxleim  11822  xrmaxifle  11824  xrmaxiflemab  11825  xrmaxiflemlub  11826  xrmaxiflemcom  11827  xrmaxltsup  11836  xrmaxadd  11839  xrminmax  11843  xrbdtri  11854  climrecvg1n  11926  serf0  11930  zsumdc  11963  isumss  11970  fisumss  11971  fsum3cvg3  11975  fsumcl2lem  11977  fsumadd  11985  fsummulc2  12027  divcnv  12076  cvgratz  12111  mertenslem2  12115  zproddc  12158  fprodssdc  12169  fprodmul  12170  fprodsplitdc  12175  fprodcl2lem  12184  fprodle  12219  fprodmodd  12220  p1modz1  12373  dvds2ln  12403  divalglemeunn  12500  divalglemeuneg  12502  bitsfzolem  12533  dvdsbnd  12545  bezoutlemnewy  12585  bezoutlemstep  12586  bezoutlemmain  12587  bezoutlembi  12594  dfgcd3  12599  uzwodc  12626  nninfctlemfo  12629  lcmgcdlem  12667  cncongr1  12693  cncongr2  12694  isprm5  12732  odzdvds  12836  pclemdc  12879  pceu  12886  dvdsprmpweqle  12928  pcadd  12931  1arith  12958  4sqexercise2  12990  4sqlem13m  12994  ennnfonelemhom  13054  ennnfonelemrnh  13055  ctinfomlemom  13066  prdsval  13374  resmhm2b  13590  mhmid  13720  mhmmnd  13721  ghmgrp  13723  mulgfng  13729  conjnmzb  13885  imasabl  13941  issrg  13997  ringinvnzdiv  14082  znunit  14692  psrval  14699  mplsubgfilemcl  14732  cnpnei  14962  cnntr  14968  cncnp  14973  lmtopcnp  14993  txdis1cn  15021  xmettxlem  15252  metcnp3  15254  fsumcncntop  15310  cncfco  15334  mulcncf  15351  dedekindeulemuub  15360  dedekindeulemlu  15364  dedekindicclemuub  15369  dedekindicclemlu  15373  dedekindicclemicc  15375  ivthinclemlr  15380  ivthinclemur  15382  limcimo  15408  cnplimcim  15410  plymullem1  15491  plycolemc  15501  plycj  15504  dvply2g  15509  pilem3  15526  lgsfcl2  15754  lgsval2lem  15758  lgsdir  15783  lgsne0  15786  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  lgsquad3  15832  umgrvad2edg  16081  usgredg2vlem2  16093  wlkvtxiedg  16215  wlkvtxiedgg  16216  clwwlkccatlem  16270  eupth2lem3lem4fi  16343  eupth2lemsfi  16348  peano4nninf  16659  nnnninfex  16675  trilpolemeq1  16695  gfsumval  16732  gfsumcl  16739