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  4077  tfr1onlemaccex  6492  tfrcllemaccex  6505  phplem4on  7025  dif1enen  7038  en2eqpr  7065  unsnfidcex  7078  unsnfidcel  7079  unfidisj  7080  undifdc  7082  fiintim  7089  ssfirab  7094  suplub2ti  7164  djudom  7256  omp1eomlem  7257  difinfsnlem  7262  difinfinf  7264  ctssdclemn0  7273  ctssdc  7276  nnnninfeq2  7292  nninfisol  7296  nninfwlpoimlemginf  7339  cc3  7450  ltaddpr  7780  ltexprlemrl  7793  addcanprleml  7797  addcanprlemu  7798  aptiprleml  7822  aptiprlemu  7823  cauappcvgprlemdisj  7834  cauappcvgprlemladdrl  7840  caucvgprlemloc  7858  caucvgprlemladdrl  7861  caucvgprprlemopl  7880  caucvgprprlemloc  7886  caucvgprprlemexbt  7889  suplocexprlemrl  7900  suplocexprlemru  7902  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemub  7906  caucvgsrlemoffres  7983  suplocsrlem  7991  axcaucvglemcau  8081  axcaucvglemres  8082  negf1o  8524  apreim  8746  apsym  8749  apcotr  8750  apadd1  8751  apneg  8754  mulext1  8755  mulge0  8762  apti  8765  aprcl  8789  qapne  9830  xaddf  10036  xaddval  10037  zsupcllemstep  10444  qtri3or  10455  exbtwnzlemstep  10462  rebtwn2zlemstep  10467  addmodlteq  10615  seq3f1olemqsumk  10729  seq3f1oleml  10733  qsqeqor  10867  apexp1  10935  faclbnd  10958  hashennnuni  10996  swrdswrd  11232  swrdccatin1  11252  pfxccatin12lem3  11259  swrdccat3blem  11266  cvg1nlemres  11491  resqrexlemoverl  11527  resqrexlemglsq  11528  resqrexlemga  11529  minmax  11736  xrmaxleim  11750  xrmaxifle  11752  xrmaxiflemab  11753  xrmaxiflemlub  11754  xrmaxiflemcom  11755  xrmaxltsup  11764  xrmaxadd  11767  xrminmax  11771  xrbdtri  11782  climrecvg1n  11854  serf0  11858  zsumdc  11890  isumss  11897  fisumss  11898  fsum3cvg3  11902  fsumcl2lem  11904  fsumadd  11912  fsummulc2  11954  divcnv  12003  cvgratz  12038  mertenslem2  12042  zproddc  12085  fprodssdc  12096  fprodmul  12097  fprodsplitdc  12102  fprodcl2lem  12111  fprodle  12146  fprodmodd  12147  p1modz1  12300  dvds2ln  12330  divalglemeunn  12427  divalglemeuneg  12429  bitsfzolem  12460  dvdsbnd  12472  bezoutlemnewy  12512  bezoutlemstep  12513  bezoutlemmain  12514  bezoutlembi  12521  dfgcd3  12526  uzwodc  12553  nninfctlemfo  12556  lcmgcdlem  12594  cncongr1  12620  cncongr2  12621  isprm5  12659  odzdvds  12763  pclemdc  12806  pceu  12813  dvdsprmpweqle  12855  pcadd  12858  1arith  12885  4sqexercise2  12917  4sqlem13m  12921  ennnfonelemhom  12981  ennnfonelemrnh  12982  ctinfomlemom  12993  prdsval  13301  resmhm2b  13517  mhmid  13647  mhmmnd  13648  ghmgrp  13650  mulgfng  13656  conjnmzb  13812  imasabl  13868  issrg  13923  ringinvnzdiv  14008  znunit  14617  psrval  14624  mplsubgfilemcl  14657  cnpnei  14887  cnntr  14893  cncnp  14898  lmtopcnp  14918  txdis1cn  14946  xmettxlem  15177  metcnp3  15179  fsumcncntop  15235  cncfco  15259  mulcncf  15276  dedekindeulemuub  15285  dedekindeulemlu  15289  dedekindicclemuub  15294  dedekindicclemlu  15298  dedekindicclemicc  15300  ivthinclemlr  15305  ivthinclemur  15307  limcimo  15333  cnplimcim  15335  plymullem1  15416  plycolemc  15426  plycj  15429  dvply2g  15434  pilem3  15451  lgsfcl2  15679  lgsval2lem  15683  lgsdir  15708  lgsne0  15711  gausslemma2dlem1a  15731  gausslemma2dlem1f1o  15733  lgsquad3  15757  umgrvad2edg  16003  usgredg2vlem2  16015  wlkvtxiedgg  16042  peano4nninf  16331  nnnninfex  16347  trilpolemeq1  16367