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  4088  tfr1onlemaccex  6557  tfrcllemaccex  6570  phplem4on  7097  dif1enen  7112  elssdc  7137  en2eqpr  7142  unsnfidcex  7155  unsnfidcel  7156  unfidisj  7157  undifdc  7159  fiintim  7166  ssfirab  7172  suplub2ti  7243  djudom  7335  omp1eomlem  7336  difinfsnlem  7341  difinfinf  7343  ctssdclemn0  7352  ctssdc  7355  nnnninfeq2  7371  nninfisol  7375  nninfwlpoimlemginf  7418  cc3  7530  ltaddpr  7860  ltexprlemrl  7873  addcanprleml  7877  addcanprlemu  7878  aptiprleml  7902  aptiprlemu  7903  cauappcvgprlemdisj  7914  cauappcvgprlemladdrl  7920  caucvgprlemloc  7938  caucvgprlemladdrl  7941  caucvgprprlemopl  7960  caucvgprprlemloc  7966  caucvgprprlemexbt  7969  suplocexprlemrl  7980  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemub  7986  caucvgsrlemoffres  8063  suplocsrlem  8071  axcaucvglemcau  8161  axcaucvglemres  8162  negf1o  8603  apreim  8825  apsym  8828  apcotr  8829  apadd1  8830  apneg  8833  mulext1  8834  mulge0  8841  apti  8844  aprcl  8868  qapne  9917  xaddf  10123  xaddval  10124  zsupcllemstep  10535  qtri3or  10546  exbtwnzlemstep  10553  rebtwn2zlemstep  10558  addmodlteq  10706  seq3f1olemqsumk  10820  seq3f1oleml  10824  qsqeqor  10958  apexp1  11026  faclbnd  11049  hashennnuni  11087  swrdswrd  11335  swrdccatin1  11355  pfxccatin12lem3  11362  swrdccat3blem  11369  cvg1nlemres  11608  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemga  11646  minmax  11853  xrmaxleim  11867  xrmaxifle  11869  xrmaxiflemab  11870  xrmaxiflemlub  11871  xrmaxiflemcom  11872  xrmaxltsup  11881  xrmaxadd  11884  xrminmax  11888  xrbdtri  11899  climrecvg1n  11971  serf0  11975  zsumdc  12008  isumss  12015  fisumss  12016  fsum3cvg3  12020  fsumcl2lem  12022  fsumadd  12030  fsummulc2  12072  divcnv  12121  cvgratz  12156  mertenslem2  12160  zproddc  12203  fprodssdc  12214  fprodmul  12215  fprodsplitdc  12220  fprodcl2lem  12229  fprodle  12264  fprodmodd  12265  p1modz1  12418  dvds2ln  12448  divalglemeunn  12545  divalglemeuneg  12547  bitsfzolem  12578  dvdsbnd  12590  bezoutlemnewy  12630  bezoutlemstep  12631  bezoutlemmain  12632  bezoutlembi  12639  dfgcd3  12644  uzwodc  12671  nninfctlemfo  12674  lcmgcdlem  12712  cncongr1  12738  cncongr2  12739  isprm5  12777  odzdvds  12881  pclemdc  12924  pceu  12931  dvdsprmpweqle  12973  pcadd  12976  1arith  13003  4sqexercise2  13035  4sqlem13m  13039  ennnfonelemhom  13099  ennnfonelemrnh  13100  ctinfomlemom  13111  prdsval  13419  resmhm2b  13635  mhmid  13765  mhmmnd  13766  ghmgrp  13768  mulgfng  13774  conjnmzb  13930  imasabl  13986  issrg  14042  ringinvnzdiv  14127  znunit  14738  psrval  14745  mplsubgfilemcl  14783  cnpnei  15013  cnntr  15019  cncnp  15024  lmtopcnp  15044  txdis1cn  15072  xmettxlem  15303  metcnp3  15305  fsumcncntop  15361  cncfco  15385  mulcncf  15402  dedekindeulemuub  15411  dedekindeulemlu  15415  dedekindicclemuub  15420  dedekindicclemlu  15424  dedekindicclemicc  15426  ivthinclemlr  15431  ivthinclemur  15433  limcimo  15459  cnplimcim  15461  plymullem1  15542  plycolemc  15552  plycj  15555  dvply2g  15560  pilem3  15577  lgsfcl2  15808  lgsval2lem  15812  lgsdir  15837  lgsne0  15840  gausslemma2dlem1a  15860  gausslemma2dlem1f1o  15862  lgsquad3  15886  umgrvad2edg  16135  usgredg2vlem2  16147  wlkvtxiedg  16269  wlkvtxiedgg  16270  clwwlkccatlem  16324  eupth2lem3lem4fi  16397  eupth2lemsfi  16402  peano4nninf  16715  nnnninfex  16731  trilpolemeq1  16755  gfsumval  16792  gfsumcl  16799