Theorem ad3antrrr 496

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 492	1 |- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad4antr  498  ad5ant12  522  disjiun  4125  tfr1onlemaccex  6619  tfrcllemaccex  6632  phplem4on  7169  dif1enen  7184  elssdc  7209  en2eqpr  7214  unsnfidcex  7227  unsnfidcel  7228  unfidisj  7229  undifdc  7231  fiintim  7238  ssfirab  7244  suplub2ti  7342  djudom  7434  omp1eomlem  7435  difinfsnlem  7440  difinfinf  7442  ctssdclemn0  7451  ctssdc  7454  nnnninfeq2  7470  nninfisol  7474  nninfwlpoimlemginf  7517  cc3  7635  ltaddpr  7965  ltexprlemrl  7978  addcanprleml  7982  addcanprlemu  7983  aptiprleml  8007  aptiprlemu  8008  cauappcvgprlemdisj  8019  cauappcvgprlemladdrl  8025  caucvgprlemloc  8043  caucvgprlemladdrl  8046  caucvgprprlemopl  8065  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  suplocexprlemrl  8085  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  caucvgsrlemoffres  8168  suplocsrlem  8176  axcaucvglemcau  8266  axcaucvglemres  8267  negf1o  8711  apreim  8934  apsym  8937  apcotr  8938  apadd1  8939  apneg  8942  mulext1  8943  mulge0  8950  apti  8953  aprcl  8977  qapne  10049  xaddf  10257  xaddval  10258  zsupcllemstep  10673  qtri3or  10686  exbtwnzlemstep  10693  rebtwn2zlemstep  10698  addmodlteq  10850  seq3f1olemqsumk  10964  seq3f1oleml  10968  qsqeqor  11102  apexp1  11172  faclbnd  11195  hashennnuni  11234  swrdswrd  11493  swrdccatin1  11513  pfxccatin12lem3  11520  swrdccat3blem  11527  cvg1nlemres  11767  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemga  11805  fiidxsupcl  12012  minmax  12014  xrmaxleim  12029  xrmaxifle  12031  xrmaxiflemab  12032  xrmaxiflemlub  12033  xrmaxiflemcom  12034  xrmaxltsup  12043  xrmaxadd  12046  xrminmax  12050  xrbdtri  12061  climrecvg1n  12133  serf0  12137  zsumdc  12170  isumss  12177  fisumss  12178  fsum3cvg3  12182  fsumcl2lem  12184  fsumadd  12192  fsummulc2  12234  divcnv  12283  cvgratz  12318  mertenslem2  12322  zproddc  12365  fprodssdc  12376  fprodmul  12377  fprodsplitdc  12382  fprodcl2lem  12391  fprodle  12426  fprodmodd  12427  p1modz1  12580  dvds2ln  12610  divalglemeunn  12707  divalglemeuneg  12709  bitsfzolem  12740  dvdsbnd  12752  bezoutlemnewy  12792  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlembi  12801  dfgcd3  12806  uzwodc  12833  nninfctlemfo  12836  lcmgcdlem  12874  cncongr1  12900  cncongr2  12901  isprm5  12940  sqrtrirr  13008  odzdvds  13047  pclemdc  13090  pceu  13097  dvdsprmpweqle  13139  pcadd  13142  1arith  13169  4sqexercise2  13201  4sqlem13m  13205  ballotfilemcdc  13275  ballotfilemsle  13300  ennnfonelemhom  13358  ennnfonelemrnh  13359  ctinfomlemom  13370  resmhm2b  13849  mhmid  13971  mhmmnd  13972  ghmgrp  13974  mulgfng  13980  conjnmzb  14136  imasabl  14224  gsumvalfi  14236  gsumclfi  14243  gsummptfidmadd  14245  gsumsubmclfi  14247  gsumconstcmn  14250  prdsval  14257  issrg  14353  ringinvnzdiv  14439  znunit  15078  psrval  15134  psrbaglefifi  15147  mplsubgfilemcl  15181  cnpnei  15411  cnntr  15417  cncnp  15422  lmtopcnp  15442  txdis1cn  15470  xmettxlem  15701  metcnp3  15703  fsumcncntop  15759  cncfco  15783  mulcncf  15800  dedekindeulemuub  15809  dedekindeulemlu  15813  dedekindicclemuub  15818  dedekindicclemlu  15822  dedekindicclemicc  15824  ivthinclemlr  15829  ivthinclemur  15831  limcimo  15857  cnplimcim  15859  plymullem1  15940  plycolemc  15950  plycj  15953  dvply2g  15958  pilem3  15976  lgsfcl2  16291  lgsval2lem  16295  lgsdir  16320  lgsne0  16323  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  lgsquad3  16369  umgrvad2edg  16618  usgredg2vlem2  16630  wlkvtxiedg  16752  wlkvtxiedgg  16753  clwwlkccatlem  16807  eupth2lem3lem4fi  16880  eupth2lemsfi  16885  peano4nninf  17215  nnnninfex  17231  trilpolemeq1  17256