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  4029  tfr1onlemaccex  6415  tfrcllemaccex  6428  phplem4on  6937  dif1enen  6950  en2eqpr  6977  unsnfidcex  6990  unsnfidcel  6991  unfidisj  6992  undifdc  6994  fiintim  7001  ssfirab  7006  suplub2ti  7076  djudom  7168  omp1eomlem  7169  difinfsnlem  7174  difinfinf  7176  ctssdclemn0  7185  ctssdc  7188  nnnninfeq2  7204  nninfisol  7208  nninfwlpoimlemginf  7251  cc3  7353  ltaddpr  7683  ltexprlemrl  7696  addcanprleml  7700  addcanprlemu  7701  aptiprleml  7725  aptiprlemu  7726  cauappcvgprlemdisj  7737  cauappcvgprlemladdrl  7743  caucvgprlemloc  7761  caucvgprlemladdrl  7764  caucvgprprlemopl  7783  caucvgprprlemloc  7789  caucvgprprlemexbt  7792  suplocexprlemrl  7803  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  caucvgsrlemoffres  7886  suplocsrlem  7894  axcaucvglemcau  7984  axcaucvglemres  7985  negf1o  8427  apreim  8649  apsym  8652  apcotr  8653  apadd1  8654  apneg  8657  mulext1  8658  mulge0  8665  apti  8668  aprcl  8692  qapne  9732  xaddf  9938  xaddval  9939  zsupcllemstep  10338  qtri3or  10349  exbtwnzlemstep  10356  rebtwn2zlemstep  10361  addmodlteq  10509  seq3f1olemqsumk  10623  seq3f1oleml  10627  qsqeqor  10761  apexp1  10829  faclbnd  10852  hashennnuni  10890  cvg1nlemres  11169  resqrexlemoverl  11205  resqrexlemglsq  11206  resqrexlemga  11207  minmax  11414  xrmaxleim  11428  xrmaxifle  11430  xrmaxiflemab  11431  xrmaxiflemlub  11432  xrmaxiflemcom  11433  xrmaxltsup  11442  xrmaxadd  11445  xrminmax  11449  xrbdtri  11460  climrecvg1n  11532  serf0  11536  zsumdc  11568  isumss  11575  fisumss  11576  fsum3cvg3  11580  fsumcl2lem  11582  fsumadd  11590  fsummulc2  11632  divcnv  11681  cvgratz  11716  mertenslem2  11720  zproddc  11763  fprodssdc  11774  fprodmul  11775  fprodsplitdc  11780  fprodcl2lem  11789  fprodle  11824  fprodmodd  11825  p1modz1  11978  dvds2ln  12008  divalglemeunn  12105  divalglemeuneg  12107  bitsfzolem  12138  dvdsbnd  12150  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlembi  12199  dfgcd3  12204  uzwodc  12231  nninfctlemfo  12234  lcmgcdlem  12272  cncongr1  12298  cncongr2  12299  isprm5  12337  odzdvds  12441  pclemdc  12484  pceu  12491  dvdsprmpweqle  12533  pcadd  12536  1arith  12563  4sqexercise2  12595  4sqlem13m  12599  ennnfonelemhom  12659  ennnfonelemrnh  12660  ctinfomlemom  12671  prdsval  12977  resmhm2b  13193  mhmid  13323  mhmmnd  13324  ghmgrp  13326  mulgfng  13332  conjnmzb  13488  imasabl  13544  issrg  13599  ringinvnzdiv  13684  znunit  14293  psrval  14300  mplsubgfilemcl  14333  cnpnei  14563  cnntr  14569  cncnp  14574  lmtopcnp  14594  txdis1cn  14622  xmettxlem  14853  metcnp3  14855  fsumcncntop  14911  cncfco  14935  mulcncf  14952  dedekindeulemuub  14961  dedekindeulemlu  14965  dedekindicclemuub  14970  dedekindicclemlu  14974  dedekindicclemicc  14976  ivthinclemlr  14981  ivthinclemur  14983  limcimo  15009  cnplimcim  15011  plymullem1  15092  plycolemc  15102  plycj  15105  dvply2g  15110  pilem3  15127  lgsfcl2  15355  lgsval2lem  15359  lgsdir  15384  lgsne0  15387  gausslemma2dlem1a  15407  gausslemma2dlem1f1o  15409  lgsquad3  15433  peano4nninf  15761  nnnninfex  15777  trilpolemeq1  15797