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  4078  tfr1onlemaccex  6500  tfrcllemaccex  6513  phplem4on  7037  dif1enen  7050  elssdc  7075  en2eqpr  7080  unsnfidcex  7093  unsnfidcel  7094  unfidisj  7095  undifdc  7097  fiintim  7104  ssfirab  7109  suplub2ti  7179  djudom  7271  omp1eomlem  7272  difinfsnlem  7277  difinfinf  7279  ctssdclemn0  7288  ctssdc  7291  nnnninfeq2  7307  nninfisol  7311  nninfwlpoimlemginf  7354  cc3  7465  ltaddpr  7795  ltexprlemrl  7808  addcanprleml  7812  addcanprlemu  7813  aptiprleml  7837  aptiprlemu  7838  cauappcvgprlemdisj  7849  cauappcvgprlemladdrl  7855  caucvgprlemloc  7873  caucvgprlemladdrl  7876  caucvgprprlemopl  7895  caucvgprprlemloc  7901  caucvgprprlemexbt  7904  suplocexprlemrl  7915  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  caucvgsrlemoffres  7998  suplocsrlem  8006  axcaucvglemcau  8096  axcaucvglemres  8097  negf1o  8539  apreim  8761  apsym  8764  apcotr  8765  apadd1  8766  apneg  8769  mulext1  8770  mulge0  8777  apti  8780  aprcl  8804  qapne  9846  xaddf  10052  xaddval  10053  zsupcllemstep  10461  qtri3or  10472  exbtwnzlemstep  10479  rebtwn2zlemstep  10484  addmodlteq  10632  seq3f1olemqsumk  10746  seq3f1oleml  10750  qsqeqor  10884  apexp1  10952  faclbnd  10975  hashennnuni  11013  swrdswrd  11252  swrdccatin1  11272  pfxccatin12lem3  11279  swrdccat3blem  11286  cvg1nlemres  11511  resqrexlemoverl  11547  resqrexlemglsq  11548  resqrexlemga  11549  minmax  11756  xrmaxleim  11770  xrmaxifle  11772  xrmaxiflemab  11773  xrmaxiflemlub  11774  xrmaxiflemcom  11775  xrmaxltsup  11784  xrmaxadd  11787  xrminmax  11791  xrbdtri  11802  climrecvg1n  11874  serf0  11878  zsumdc  11910  isumss  11917  fisumss  11918  fsum3cvg3  11922  fsumcl2lem  11924  fsumadd  11932  fsummulc2  11974  divcnv  12023  cvgratz  12058  mertenslem2  12062  zproddc  12105  fprodssdc  12116  fprodmul  12117  fprodsplitdc  12122  fprodcl2lem  12131  fprodle  12166  fprodmodd  12167  p1modz1  12320  dvds2ln  12350  divalglemeunn  12447  divalglemeuneg  12449  bitsfzolem  12480  dvdsbnd  12492  bezoutlemnewy  12532  bezoutlemstep  12533  bezoutlemmain  12534  bezoutlembi  12541  dfgcd3  12546  uzwodc  12573  nninfctlemfo  12576  lcmgcdlem  12614  cncongr1  12640  cncongr2  12641  isprm5  12679  odzdvds  12783  pclemdc  12826  pceu  12833  dvdsprmpweqle  12875  pcadd  12878  1arith  12905  4sqexercise2  12937  4sqlem13m  12941  ennnfonelemhom  13001  ennnfonelemrnh  13002  ctinfomlemom  13013  prdsval  13321  resmhm2b  13537  mhmid  13667  mhmmnd  13668  ghmgrp  13670  mulgfng  13676  conjnmzb  13832  imasabl  13888  issrg  13943  ringinvnzdiv  14028  znunit  14638  psrval  14645  mplsubgfilemcl  14678  cnpnei  14908  cnntr  14914  cncnp  14919  lmtopcnp  14939  txdis1cn  14967  xmettxlem  15198  metcnp3  15200  fsumcncntop  15256  cncfco  15280  mulcncf  15297  dedekindeulemuub  15306  dedekindeulemlu  15310  dedekindicclemuub  15315  dedekindicclemlu  15319  dedekindicclemicc  15321  ivthinclemlr  15326  ivthinclemur  15328  limcimo  15354  cnplimcim  15356  plymullem1  15437  plycolemc  15447  plycj  15450  dvply2g  15455  pilem3  15472  lgsfcl2  15700  lgsval2lem  15704  lgsdir  15729  lgsne0  15732  gausslemma2dlem1a  15752  gausslemma2dlem1f1o  15754  lgsquad3  15778  umgrvad2edg  16024  usgredg2vlem2  16036  wlkvtxiedg  16086  wlkvtxiedgg  16087  clwwlkccatlem  16137  peano4nninf  16432  nnnninfex  16448  trilpolemeq1  16468