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  4038  tfr1onlemaccex  6433  tfrcllemaccex  6446  phplem4on  6963  dif1enen  6976  en2eqpr  7003  unsnfidcex  7016  unsnfidcel  7017  unfidisj  7018  undifdc  7020  fiintim  7027  ssfirab  7032  suplub2ti  7102  djudom  7194  omp1eomlem  7195  difinfsnlem  7200  difinfinf  7202  ctssdclemn0  7211  ctssdc  7214  nnnninfeq2  7230  nninfisol  7234  nninfwlpoimlemginf  7277  cc3  7379  ltaddpr  7709  ltexprlemrl  7722  addcanprleml  7726  addcanprlemu  7727  aptiprleml  7751  aptiprlemu  7752  cauappcvgprlemdisj  7763  cauappcvgprlemladdrl  7769  caucvgprlemloc  7787  caucvgprlemladdrl  7790  caucvgprprlemopl  7809  caucvgprprlemloc  7815  caucvgprprlemexbt  7818  suplocexprlemrl  7829  suplocexprlemru  7831  suplocexprlemdisj  7832  suplocexprlemloc  7833  suplocexprlemub  7835  caucvgsrlemoffres  7912  suplocsrlem  7920  axcaucvglemcau  8010  axcaucvglemres  8011  negf1o  8453  apreim  8675  apsym  8678  apcotr  8679  apadd1  8680  apneg  8683  mulext1  8684  mulge0  8691  apti  8694  aprcl  8718  qapne  9759  xaddf  9965  xaddval  9966  zsupcllemstep  10370  qtri3or  10381  exbtwnzlemstep  10388  rebtwn2zlemstep  10393  addmodlteq  10541  seq3f1olemqsumk  10655  seq3f1oleml  10659  qsqeqor  10793  apexp1  10861  faclbnd  10884  hashennnuni  10922  cvg1nlemres  11238  resqrexlemoverl  11274  resqrexlemglsq  11275  resqrexlemga  11276  minmax  11483  xrmaxleim  11497  xrmaxifle  11499  xrmaxiflemab  11500  xrmaxiflemlub  11501  xrmaxiflemcom  11502  xrmaxltsup  11511  xrmaxadd  11514  xrminmax  11518  xrbdtri  11529  climrecvg1n  11601  serf0  11605  zsumdc  11637  isumss  11644  fisumss  11645  fsum3cvg3  11649  fsumcl2lem  11651  fsumadd  11659  fsummulc2  11701  divcnv  11750  cvgratz  11785  mertenslem2  11789  zproddc  11832  fprodssdc  11843  fprodmul  11844  fprodsplitdc  11849  fprodcl2lem  11858  fprodle  11893  fprodmodd  11894  p1modz1  12047  dvds2ln  12077  divalglemeunn  12174  divalglemeuneg  12176  bitsfzolem  12207  dvdsbnd  12219  bezoutlemnewy  12259  bezoutlemstep  12260  bezoutlemmain  12261  bezoutlembi  12268  dfgcd3  12273  uzwodc  12300  nninfctlemfo  12303  lcmgcdlem  12341  cncongr1  12367  cncongr2  12368  isprm5  12406  odzdvds  12510  pclemdc  12553  pceu  12560  dvdsprmpweqle  12602  pcadd  12605  1arith  12632  4sqexercise2  12664  4sqlem13m  12668  ennnfonelemhom  12728  ennnfonelemrnh  12729  ctinfomlemom  12740  prdsval  13047  resmhm2b  13263  mhmid  13393  mhmmnd  13394  ghmgrp  13396  mulgfng  13402  conjnmzb  13558  imasabl  13614  issrg  13669  ringinvnzdiv  13754  znunit  14363  psrval  14370  mplsubgfilemcl  14403  cnpnei  14633  cnntr  14639  cncnp  14644  lmtopcnp  14664  txdis1cn  14692  xmettxlem  14923  metcnp3  14925  fsumcncntop  14981  cncfco  15005  mulcncf  15022  dedekindeulemuub  15031  dedekindeulemlu  15035  dedekindicclemuub  15040  dedekindicclemlu  15044  dedekindicclemicc  15046  ivthinclemlr  15051  ivthinclemur  15053  limcimo  15079  cnplimcim  15081  plymullem1  15162  plycolemc  15172  plycj  15175  dvply2g  15180  pilem3  15197  lgsfcl2  15425  lgsval2lem  15429  lgsdir  15454  lgsne0  15457  gausslemma2dlem1a  15477  gausslemma2dlem1f1o  15479  lgsquad3  15503  peano4nninf  15876  nnnninfex  15892  trilpolemeq1  15912