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  4104  tfr1onlemaccex  6579  tfrcllemaccex  6592  phplem4on  7122  dif1enen  7137  elssdc  7162  en2eqpr  7167  unsnfidcex  7180  unsnfidcel  7181  unfidisj  7182  undifdc  7184  fiintim  7191  ssfirab  7197  suplub2ti  7292  djudom  7384  omp1eomlem  7385  difinfsnlem  7390  difinfinf  7392  ctssdclemn0  7401  ctssdc  7404  nnnninfeq2  7420  nninfisol  7424  nninfwlpoimlemginf  7467  cc3  7582  ltaddpr  7912  ltexprlemrl  7925  addcanprleml  7929  addcanprlemu  7930  aptiprleml  7954  aptiprlemu  7955  cauappcvgprlemdisj  7966  cauappcvgprlemladdrl  7972  caucvgprlemloc  7990  caucvgprlemladdrl  7993  caucvgprprlemopl  8012  caucvgprprlemloc  8018  caucvgprprlemexbt  8021  suplocexprlemrl  8032  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemub  8038  caucvgsrlemoffres  8115  suplocsrlem  8123  axcaucvglemcau  8213  axcaucvglemres  8214  negf1o  8655  apreim  8877  apsym  8880  apcotr  8881  apadd1  8882  apneg  8885  mulext1  8886  mulge0  8893  apti  8896  aprcl  8920  qapne  9971  xaddf  10177  xaddval  10178  zsupcllemstep  10589  qtri3or  10600  exbtwnzlemstep  10607  rebtwn2zlemstep  10612  addmodlteq  10760  seq3f1olemqsumk  10874  seq3f1oleml  10878  qsqeqor  11012  apexp1  11080  faclbnd  11103  hashennnuni  11142  swrdswrd  11397  swrdccatin1  11417  pfxccatin12lem3  11424  swrdccat3blem  11431  cvg1nlemres  11670  resqrexlemoverl  11706  resqrexlemglsq  11707  resqrexlemga  11708  minmax  11915  xrmaxleim  11929  xrmaxifle  11931  xrmaxiflemab  11932  xrmaxiflemlub  11933  xrmaxiflemcom  11934  xrmaxltsup  11943  xrmaxadd  11946  xrminmax  11950  xrbdtri  11961  climrecvg1n  12033  serf0  12037  zsumdc  12070  isumss  12077  fisumss  12078  fsum3cvg3  12082  fsumcl2lem  12084  fsumadd  12092  fsummulc2  12134  divcnv  12183  cvgratz  12218  mertenslem2  12222  zproddc  12265  fprodssdc  12276  fprodmul  12277  fprodsplitdc  12282  fprodcl2lem  12291  fprodle  12326  fprodmodd  12327  p1modz1  12480  dvds2ln  12510  divalglemeunn  12607  divalglemeuneg  12609  bitsfzolem  12640  dvdsbnd  12652  bezoutlemnewy  12692  bezoutlemstep  12693  bezoutlemmain  12694  bezoutlembi  12701  dfgcd3  12706  uzwodc  12733  nninfctlemfo  12736  lcmgcdlem  12774  cncongr1  12800  cncongr2  12801  isprm5  12839  odzdvds  12943  pclemdc  12986  pceu  12993  dvdsprmpweqle  13035  pcadd  13038  1arith  13065  4sqexercise2  13097  4sqlem13m  13101  ennnfonelemhom  13166  ennnfonelemrnh  13167  ctinfomlemom  13178  prdsval  13486  resmhm2b  13702  mhmid  13832  mhmmnd  13833  ghmgrp  13835  mulgfng  13841  conjnmzb  13997  imasabl  14053  issrg  14109  ringinvnzdiv  14194  znunit  14807  psrval  14814  mplsubgfilemcl  14854  cnpnei  15084  cnntr  15090  cncnp  15095  lmtopcnp  15115  txdis1cn  15143  xmettxlem  15374  metcnp3  15376  fsumcncntop  15432  cncfco  15456  mulcncf  15473  dedekindeulemuub  15482  dedekindeulemlu  15486  dedekindicclemuub  15491  dedekindicclemlu  15495  dedekindicclemicc  15497  ivthinclemlr  15502  ivthinclemur  15504  limcimo  15530  cnplimcim  15532  plymullem1  15613  plycolemc  15623  plycj  15626  dvply2g  15631  pilem3  15648  lgsfcl2  15879  lgsval2lem  15883  lgsdir  15908  lgsne0  15911  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  lgsquad3  15957  umgrvad2edg  16206  usgredg2vlem2  16218  wlkvtxiedg  16340  wlkvtxiedgg  16341  clwwlkccatlem  16395  eupth2lem3lem4fi  16468  eupth2lemsfi  16473  peano4nninf  16784  nnnninfex  16800  trilpolemeq1  16824  trimul0or  16845  gfsumval  16862  gfsumcl  16870