Theorem ad3antrrr 489

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 274	. 2 |- ( ( ph /\ ch ) -> ps )
3	2	ad2antrr 485	1 |- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad4antr  491  ad5ant12  515  disjiun  3984  tfr1onlemaccex  6327  tfrcllemaccex  6340  phplem4on  6845  dif1enen  6858  en2eqpr  6885  unsnfidcex  6897  unsnfidcel  6898  unfidisj  6899  undifdc  6901  fiintim  6906  ssfirab  6911  suplub2ti  6978  djudom  7070  omp1eomlem  7071  difinfsnlem  7076  difinfinf  7078  ctssdclemn0  7087  ctssdc  7090  nnnninfeq2  7105  nninfisol  7109  nninfwlpoimlemginf  7152  cc3  7230  ltaddpr  7559  ltexprlemrl  7572  addcanprleml  7576  addcanprlemu  7577  aptiprleml  7601  aptiprlemu  7602  cauappcvgprlemdisj  7613  cauappcvgprlemladdrl  7619  caucvgprlemloc  7637  caucvgprlemladdrl  7640  caucvgprprlemopl  7659  caucvgprprlemloc  7665  caucvgprprlemexbt  7668  suplocexprlemrl  7679  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemub  7685  caucvgsrlemoffres  7762  suplocsrlem  7770  axcaucvglemcau  7860  axcaucvglemres  7861  negf1o  8301  apreim  8522  apsym  8525  apcotr  8526  apadd1  8527  apneg  8530  mulext1  8531  mulge0  8538  apti  8541  aprcl  8565  qapne  9598  xaddf  9801  xaddval  9802  qtri3or  10199  exbtwnzlemstep  10204  rebtwn2zlemstep  10209  addmodlteq  10354  seq3f1olemqsumk  10455  seq3f1oleml  10459  qsqeqor  10586  apexp1  10652  faclbnd  10675  hashennnuni  10713  cvg1nlemres  10949  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemga  10987  minmax  11193  xrmaxleim  11207  xrmaxifle  11209  xrmaxiflemab  11210  xrmaxiflemlub  11211  xrmaxiflemcom  11212  xrmaxltsup  11221  xrmaxadd  11224  xrminmax  11228  xrbdtri  11239  climrecvg1n  11311  serf0  11315  zsumdc  11347  isumss  11354  fisumss  11355  fsum3cvg3  11359  fsumcl2lem  11361  fsumadd  11369  fsummulc2  11411  divcnv  11460  cvgratz  11495  mertenslem2  11499  zproddc  11542  fprodssdc  11553  fprodmul  11554  fprodsplitdc  11559  fprodcl2lem  11568  fprodle  11603  fprodmodd  11604  p1modz1  11756  dvds2ln  11786  divalglemeunn  11880  divalglemeuneg  11882  zsupcllemstep  11900  dvdsbnd  11911  bezoutlemnewy  11951  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlembi  11960  dfgcd3  11965  uzwodc  11992  lcmgcdlem  12031  cncongr1  12057  cncongr2  12058  isprm5  12096  odzdvds  12199  pclemdc  12242  pceu  12249  dvdsprmpweqle  12290  pcadd  12293  1arith  12319  ennnfonelemhom  12370  ennnfonelemrnh  12371  ctinfomlemom  12382  cnpnei  13013  cnntr  13019  cncnp  13024  lmtopcnp  13044  txdis1cn  13072  xmettxlem  13303  metcnp3  13305  fsumcncntop  13350  cncfco  13372  mulcncf  13385  dedekindeulemuub  13389  dedekindeulemlu  13393  dedekindicclemuub  13398  dedekindicclemlu  13402  dedekindicclemicc  13404  ivthinclemlr  13409  ivthinclemur  13411  limcimo  13428  cnplimcim  13430  pilem3  13498  lgsfcl2  13701  lgsval2lem  13705  lgsdir  13730  lgsne0  13733  peano4nninf  14039  trilpolemeq1  14072