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  4083  tfr1onlemaccex  6513  tfrcllemaccex  6526  phplem4on  7053  dif1enen  7068  elssdc  7093  en2eqpr  7098  unsnfidcex  7111  unsnfidcel  7112  unfidisj  7113  undifdc  7115  fiintim  7122  ssfirab  7128  suplub2ti  7199  djudom  7291  omp1eomlem  7292  difinfsnlem  7297  difinfinf  7299  ctssdclemn0  7308  ctssdc  7311  nnnninfeq2  7327  nninfisol  7331  nninfwlpoimlemginf  7374  cc3  7486  ltaddpr  7816  ltexprlemrl  7829  addcanprleml  7833  addcanprlemu  7834  aptiprleml  7858  aptiprlemu  7859  cauappcvgprlemdisj  7870  cauappcvgprlemladdrl  7876  caucvgprlemloc  7894  caucvgprlemladdrl  7897  caucvgprprlemopl  7916  caucvgprprlemloc  7922  caucvgprprlemexbt  7925  suplocexprlemrl  7936  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemub  7942  caucvgsrlemoffres  8019  suplocsrlem  8027  axcaucvglemcau  8117  axcaucvglemres  8118  negf1o  8560  apreim  8782  apsym  8785  apcotr  8786  apadd1  8787  apneg  8790  mulext1  8791  mulge0  8798  apti  8801  aprcl  8825  qapne  9872  xaddf  10078  xaddval  10079  zsupcllemstep  10488  qtri3or  10499  exbtwnzlemstep  10506  rebtwn2zlemstep  10511  addmodlteq  10659  seq3f1olemqsumk  10773  seq3f1oleml  10777  qsqeqor  10911  apexp1  10979  faclbnd  11002  hashennnuni  11040  swrdswrd  11285  swrdccatin1  11305  pfxccatin12lem3  11312  swrdccat3blem  11319  cvg1nlemres  11545  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemga  11583  minmax  11790  xrmaxleim  11804  xrmaxifle  11806  xrmaxiflemab  11807  xrmaxiflemlub  11808  xrmaxiflemcom  11809  xrmaxltsup  11818  xrmaxadd  11821  xrminmax  11825  xrbdtri  11836  climrecvg1n  11908  serf0  11912  zsumdc  11944  isumss  11951  fisumss  11952  fsum3cvg3  11956  fsumcl2lem  11958  fsumadd  11966  fsummulc2  12008  divcnv  12057  cvgratz  12092  mertenslem2  12096  zproddc  12139  fprodssdc  12150  fprodmul  12151  fprodsplitdc  12156  fprodcl2lem  12165  fprodle  12200  fprodmodd  12201  p1modz1  12354  dvds2ln  12384  divalglemeunn  12481  divalglemeuneg  12483  bitsfzolem  12514  dvdsbnd  12526  bezoutlemnewy  12566  bezoutlemstep  12567  bezoutlemmain  12568  bezoutlembi  12575  dfgcd3  12580  uzwodc  12607  nninfctlemfo  12610  lcmgcdlem  12648  cncongr1  12674  cncongr2  12675  isprm5  12713  odzdvds  12817  pclemdc  12860  pceu  12867  dvdsprmpweqle  12909  pcadd  12912  1arith  12939  4sqexercise2  12971  4sqlem13m  12975  ennnfonelemhom  13035  ennnfonelemrnh  13036  ctinfomlemom  13047  prdsval  13355  resmhm2b  13571  mhmid  13701  mhmmnd  13702  ghmgrp  13704  mulgfng  13710  conjnmzb  13866  imasabl  13922  issrg  13977  ringinvnzdiv  14062  znunit  14672  psrval  14679  mplsubgfilemcl  14712  cnpnei  14942  cnntr  14948  cncnp  14953  lmtopcnp  14973  txdis1cn  15001  xmettxlem  15232  metcnp3  15234  fsumcncntop  15290  cncfco  15314  mulcncf  15331  dedekindeulemuub  15340  dedekindeulemlu  15344  dedekindicclemuub  15349  dedekindicclemlu  15353  dedekindicclemicc  15355  ivthinclemlr  15360  ivthinclemur  15362  limcimo  15388  cnplimcim  15390  plymullem1  15471  plycolemc  15481  plycj  15484  dvply2g  15489  pilem3  15506  lgsfcl2  15734  lgsval2lem  15738  lgsdir  15763  lgsne0  15766  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  lgsquad3  15812  umgrvad2edg  16061  usgredg2vlem2  16073  wlkvtxiedg  16195  wlkvtxiedgg  16196  clwwlkccatlem  16250  peano4nninf  16608  nnnninfex  16624  trilpolemeq1  16644  gfsumval  16680