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  4081  tfr1onlemaccex  6509  tfrcllemaccex  6522  phplem4on  7049  dif1enen  7062  elssdc  7087  en2eqpr  7092  unsnfidcex  7105  unsnfidcel  7106  unfidisj  7107  undifdc  7109  fiintim  7116  ssfirab  7121  suplub2ti  7191  djudom  7283  omp1eomlem  7284  difinfsnlem  7289  difinfinf  7291  ctssdclemn0  7300  ctssdc  7303  nnnninfeq2  7319  nninfisol  7323  nninfwlpoimlemginf  7366  cc3  7477  ltaddpr  7807  ltexprlemrl  7820  addcanprleml  7824  addcanprlemu  7825  aptiprleml  7849  aptiprlemu  7850  cauappcvgprlemdisj  7861  cauappcvgprlemladdrl  7867  caucvgprlemloc  7885  caucvgprlemladdrl  7888  caucvgprprlemopl  7907  caucvgprprlemloc  7913  caucvgprprlemexbt  7916  suplocexprlemrl  7927  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemub  7933  caucvgsrlemoffres  8010  suplocsrlem  8018  axcaucvglemcau  8108  axcaucvglemres  8109  negf1o  8551  apreim  8773  apsym  8776  apcotr  8777  apadd1  8778  apneg  8781  mulext1  8782  mulge0  8789  apti  8792  aprcl  8816  qapne  9863  xaddf  10069  xaddval  10070  zsupcllemstep  10479  qtri3or  10490  exbtwnzlemstep  10497  rebtwn2zlemstep  10502  addmodlteq  10650  seq3f1olemqsumk  10764  seq3f1oleml  10768  qsqeqor  10902  apexp1  10970  faclbnd  10993  hashennnuni  11031  swrdswrd  11276  swrdccatin1  11296  pfxccatin12lem3  11303  swrdccat3blem  11310  cvg1nlemres  11536  resqrexlemoverl  11572  resqrexlemglsq  11573  resqrexlemga  11574  minmax  11781  xrmaxleim  11795  xrmaxifle  11797  xrmaxiflemab  11798  xrmaxiflemlub  11799  xrmaxiflemcom  11800  xrmaxltsup  11809  xrmaxadd  11812  xrminmax  11816  xrbdtri  11827  climrecvg1n  11899  serf0  11903  zsumdc  11935  isumss  11942  fisumss  11943  fsum3cvg3  11947  fsumcl2lem  11949  fsumadd  11957  fsummulc2  11999  divcnv  12048  cvgratz  12083  mertenslem2  12087  zproddc  12130  fprodssdc  12141  fprodmul  12142  fprodsplitdc  12147  fprodcl2lem  12156  fprodle  12191  fprodmodd  12192  p1modz1  12345  dvds2ln  12375  divalglemeunn  12472  divalglemeuneg  12474  bitsfzolem  12505  dvdsbnd  12517  bezoutlemnewy  12557  bezoutlemstep  12558  bezoutlemmain  12559  bezoutlembi  12566  dfgcd3  12571  uzwodc  12598  nninfctlemfo  12601  lcmgcdlem  12639  cncongr1  12665  cncongr2  12666  isprm5  12704  odzdvds  12808  pclemdc  12851  pceu  12858  dvdsprmpweqle  12900  pcadd  12903  1arith  12930  4sqexercise2  12962  4sqlem13m  12966  ennnfonelemhom  13026  ennnfonelemrnh  13027  ctinfomlemom  13038  prdsval  13346  resmhm2b  13562  mhmid  13692  mhmmnd  13693  ghmgrp  13695  mulgfng  13701  conjnmzb  13857  imasabl  13913  issrg  13968  ringinvnzdiv  14053  znunit  14663  psrval  14670  mplsubgfilemcl  14703  cnpnei  14933  cnntr  14939  cncnp  14944  lmtopcnp  14964  txdis1cn  14992  xmettxlem  15223  metcnp3  15225  fsumcncntop  15281  cncfco  15305  mulcncf  15322  dedekindeulemuub  15331  dedekindeulemlu  15335  dedekindicclemuub  15340  dedekindicclemlu  15344  dedekindicclemicc  15346  ivthinclemlr  15351  ivthinclemur  15353  limcimo  15379  cnplimcim  15381  plymullem1  15462  plycolemc  15472  plycj  15475  dvply2g  15480  pilem3  15497  lgsfcl2  15725  lgsval2lem  15729  lgsdir  15754  lgsne0  15757  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  lgsquad3  15803  umgrvad2edg  16050  usgredg2vlem2  16062  wlkvtxiedg  16142  wlkvtxiedgg  16143  clwwlkccatlem  16195  peano4nninf  16544  nnnninfex  16560  trilpolemeq1  16580