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  4038  tfr1onlemaccex  6424  tfrcllemaccex  6437  phplem4on  6946  dif1enen  6959  en2eqpr  6986  unsnfidcex  6999  unsnfidcel  7000  unfidisj  7001  undifdc  7003  fiintim  7010  ssfirab  7015  suplub2ti  7085  djudom  7177  omp1eomlem  7178  difinfsnlem  7183  difinfinf  7185  ctssdclemn0  7194  ctssdc  7197  nnnninfeq2  7213  nninfisol  7217  nninfwlpoimlemginf  7260  cc3  7362  ltaddpr  7692  ltexprlemrl  7705  addcanprleml  7709  addcanprlemu  7710  aptiprleml  7734  aptiprlemu  7735  cauappcvgprlemdisj  7746  cauappcvgprlemladdrl  7752  caucvgprlemloc  7770  caucvgprlemladdrl  7773  caucvgprprlemopl  7792  caucvgprprlemloc  7798  caucvgprprlemexbt  7801  suplocexprlemrl  7812  suplocexprlemru  7814  suplocexprlemdisj  7815  suplocexprlemloc  7816  suplocexprlemub  7818  caucvgsrlemoffres  7895  suplocsrlem  7903  axcaucvglemcau  7993  axcaucvglemres  7994  negf1o  8436  apreim  8658  apsym  8661  apcotr  8662  apadd1  8663  apneg  8666  mulext1  8667  mulge0  8674  apti  8677  aprcl  8701  qapne  9742  xaddf  9948  xaddval  9949  zsupcllemstep  10353  qtri3or  10364  exbtwnzlemstep  10371  rebtwn2zlemstep  10376  addmodlteq  10524  seq3f1olemqsumk  10638  seq3f1oleml  10642  qsqeqor  10776  apexp1  10844  faclbnd  10867  hashennnuni  10905  cvg1nlemres  11215  resqrexlemoverl  11251  resqrexlemglsq  11252  resqrexlemga  11253  minmax  11460  xrmaxleim  11474  xrmaxifle  11476  xrmaxiflemab  11477  xrmaxiflemlub  11478  xrmaxiflemcom  11479  xrmaxltsup  11488  xrmaxadd  11491  xrminmax  11495  xrbdtri  11506  climrecvg1n  11578  serf0  11582  zsumdc  11614  isumss  11621  fisumss  11622  fsum3cvg3  11626  fsumcl2lem  11628  fsumadd  11636  fsummulc2  11678  divcnv  11727  cvgratz  11762  mertenslem2  11766  zproddc  11809  fprodssdc  11820  fprodmul  11821  fprodsplitdc  11826  fprodcl2lem  11835  fprodle  11870  fprodmodd  11871  p1modz1  12024  dvds2ln  12054  divalglemeunn  12151  divalglemeuneg  12153  bitsfzolem  12184  dvdsbnd  12196  bezoutlemnewy  12236  bezoutlemstep  12237  bezoutlemmain  12238  bezoutlembi  12245  dfgcd3  12250  uzwodc  12277  nninfctlemfo  12280  lcmgcdlem  12318  cncongr1  12344  cncongr2  12345  isprm5  12383  odzdvds  12487  pclemdc  12530  pceu  12537  dvdsprmpweqle  12579  pcadd  12582  1arith  12609  4sqexercise2  12641  4sqlem13m  12645  ennnfonelemhom  12705  ennnfonelemrnh  12706  ctinfomlemom  12717  prdsval  13023  resmhm2b  13239  mhmid  13369  mhmmnd  13370  ghmgrp  13372  mulgfng  13378  conjnmzb  13534  imasabl  13590  issrg  13645  ringinvnzdiv  13730  znunit  14339  psrval  14346  mplsubgfilemcl  14379  cnpnei  14609  cnntr  14615  cncnp  14620  lmtopcnp  14640  txdis1cn  14668  xmettxlem  14899  metcnp3  14901  fsumcncntop  14957  cncfco  14981  mulcncf  14998  dedekindeulemuub  15007  dedekindeulemlu  15011  dedekindicclemuub  15016  dedekindicclemlu  15020  dedekindicclemicc  15022  ivthinclemlr  15027  ivthinclemur  15029  limcimo  15055  cnplimcim  15057  plymullem1  15138  plycolemc  15148  plycj  15151  dvply2g  15156  pilem3  15173  lgsfcl2  15401  lgsval2lem  15405  lgsdir  15430  lgsne0  15433  gausslemma2dlem1a  15453  gausslemma2dlem1f1o  15455  lgsquad3  15479  peano4nninf  15807  nnnninfex  15823  trilpolemeq1  15843