Theorem ad3antrrr 484

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 480	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  486  ad5ant12  510  disjiun  3977  tfr1onlemaccex  6316  tfrcllemaccex  6329  phplem4on  6833  dif1enen  6846  en2eqpr  6873  unsnfidcex  6885  unsnfidcel  6886  unfidisj  6887  undifdc  6889  fiintim  6894  ssfirab  6899  suplub2ti  6966  djudom  7058  omp1eomlem  7059  difinfsnlem  7064  difinfinf  7066  ctssdclemn0  7075  ctssdc  7078  nnnninfeq2  7093  nninfisol  7097  cc3  7209  ltaddpr  7538  ltexprlemrl  7551  addcanprleml  7555  addcanprlemu  7556  aptiprleml  7580  aptiprlemu  7581  cauappcvgprlemdisj  7592  cauappcvgprlemladdrl  7598  caucvgprlemloc  7616  caucvgprlemladdrl  7619  caucvgprprlemopl  7638  caucvgprprlemloc  7644  caucvgprprlemexbt  7647  suplocexprlemrl  7658  suplocexprlemru  7660  suplocexprlemdisj  7661  suplocexprlemloc  7662  suplocexprlemub  7664  caucvgsrlemoffres  7741  suplocsrlem  7749  axcaucvglemcau  7839  axcaucvglemres  7840  negf1o  8280  apreim  8501  apsym  8504  apcotr  8505  apadd1  8506  apneg  8509  mulext1  8510  mulge0  8517  apti  8520  aprcl  8544  qapne  9577  xaddf  9780  xaddval  9781  qtri3or  10178  exbtwnzlemstep  10183  rebtwn2zlemstep  10188  addmodlteq  10333  seq3f1olemqsumk  10434  seq3f1oleml  10438  qsqeqor  10565  apexp1  10631  faclbnd  10654  hashennnuni  10692  cvg1nlemres  10927  resqrexlemoverl  10963  resqrexlemglsq  10964  resqrexlemga  10965  minmax  11171  xrmaxleim  11185  xrmaxifle  11187  xrmaxiflemab  11188  xrmaxiflemlub  11189  xrmaxiflemcom  11190  xrmaxltsup  11199  xrmaxadd  11202  xrminmax  11206  xrbdtri  11217  climrecvg1n  11289  serf0  11293  zsumdc  11325  isumss  11332  fisumss  11333  fsum3cvg3  11337  fsumcl2lem  11339  fsumadd  11347  fsummulc2  11389  divcnv  11438  cvgratz  11473  mertenslem2  11477  zproddc  11520  fprodssdc  11531  fprodmul  11532  fprodsplitdc  11537  fprodcl2lem  11546  fprodle  11581  fprodmodd  11582  p1modz1  11734  dvds2ln  11764  divalglemeunn  11858  divalglemeuneg  11860  zsupcllemstep  11878  dvdsbnd  11889  bezoutlemnewy  11929  bezoutlemstep  11930  bezoutlemmain  11931  bezoutlembi  11938  dfgcd3  11943  uzwodc  11970  lcmgcdlem  12009  cncongr1  12035  cncongr2  12036  isprm5  12074  odzdvds  12177  pclemdc  12220  pceu  12227  dvdsprmpweqle  12268  pcadd  12271  1arith  12297  ennnfonelemhom  12348  ennnfonelemrnh  12349  ctinfomlemom  12360  cnpnei  12859  cnntr  12865  cncnp  12870  lmtopcnp  12890  txdis1cn  12918  xmettxlem  13149  metcnp3  13151  fsumcncntop  13196  cncfco  13218  mulcncf  13231  dedekindeulemuub  13235  dedekindeulemlu  13239  dedekindicclemuub  13244  dedekindicclemlu  13248  dedekindicclemicc  13250  ivthinclemlr  13255  ivthinclemur  13257  limcimo  13274  cnplimcim  13276  pilem3  13344  lgsfcl2  13547  lgsval2lem  13551  lgsdir  13576  lgsne0  13579  peano4nninf  13886  trilpolemeq1  13919