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 )

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  498  ad5ant12  522  disjiun  4120  tfr1onlemaccex  6609  tfrcllemaccex  6622  phplem4on  7159  dif1enen  7174  elssdc  7199  en2eqpr  7204  unsnfidcex  7217  unsnfidcel  7218  unfidisj  7219  undifdc  7221  fiintim  7228  ssfirab  7234  suplub2ti  7331  djudom  7423  omp1eomlem  7424  difinfsnlem  7429  difinfinf  7431  ctssdclemn0  7440  ctssdc  7443  nnnninfeq2  7459  nninfisol  7463  nninfwlpoimlemginf  7506  cc3  7624  ltaddpr  7954  ltexprlemrl  7967  addcanprleml  7971  addcanprlemu  7972  aptiprleml  7996  aptiprlemu  7997  cauappcvgprlemdisj  8008  cauappcvgprlemladdrl  8014  caucvgprlemloc  8032  caucvgprlemladdrl  8035  caucvgprprlemopl  8054  caucvgprprlemloc  8060  caucvgprprlemexbt  8063  suplocexprlemrl  8074  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemub  8080  caucvgsrlemoffres  8157  suplocsrlem  8165  axcaucvglemcau  8255  axcaucvglemres  8256  negf1o  8699  apreim  8921  apsym  8924  apcotr  8925  apadd1  8926  apneg  8929  mulext1  8930  mulge0  8937  apti  8940  aprcl  8964  qapne  10018  xaddf  10225  xaddval  10226  zsupcllemstep  10640  qtri3or  10653  exbtwnzlemstep  10660  rebtwn2zlemstep  10665  addmodlteq  10813  seq3f1olemqsumk  10927  seq3f1oleml  10931  qsqeqor  11065  apexp1  11134  faclbnd  11157  hashennnuni  11196  swrdswrd  11455  swrdccatin1  11475  pfxccatin12lem3  11482  swrdccat3blem  11489  cvg1nlemres  11729  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemga  11767  minmax  11974  xrmaxleim  11988  xrmaxifle  11990  xrmaxiflemab  11991  xrmaxiflemlub  11992  xrmaxiflemcom  11993  xrmaxltsup  12002  xrmaxadd  12005  xrminmax  12009  xrbdtri  12020  climrecvg1n  12092  serf0  12096  zsumdc  12129  isumss  12136  fisumss  12137  fsum3cvg3  12141  fsumcl2lem  12143  fsumadd  12151  fsummulc2  12193  divcnv  12242  cvgratz  12277  mertenslem2  12281  zproddc  12324  fprodssdc  12335  fprodmul  12336  fprodsplitdc  12341  fprodcl2lem  12350  fprodle  12385  fprodmodd  12386  p1modz1  12539  dvds2ln  12569  divalglemeunn  12666  divalglemeuneg  12668  bitsfzolem  12699  dvdsbnd  12711  bezoutlemnewy  12751  bezoutlemstep  12752  bezoutlemmain  12753  bezoutlembi  12760  dfgcd3  12765  uzwodc  12792  nninfctlemfo  12795  lcmgcdlem  12833  cncongr1  12859  cncongr2  12860  isprm5  12898  odzdvds  13002  pclemdc  13045  pceu  13052  dvdsprmpweqle  13094  pcadd  13097  1arith  13124  4sqexercise2  13156  4sqlem13m  13160  ballotfilemcdc  13201  ballotfilemsle  13226  ennnfonelemhom  13284  ennnfonelemrnh  13285  ctinfomlemom  13296  resmhm2b  13773  mhmid  13895  mhmmnd  13896  ghmgrp  13898  mulgfng  13904  conjnmzb  14060  imasabl  14117  gsumvalfi  14129  gsumclfi  14136  gsummptfidmadd  14138  gsumsubmclfi  14140  gsumconstcmn  14143  prdsval  14150  issrg  14243  ringinvnzdiv  14328  znunit  14966  psrval  14973  mplsubgfilemcl  15013  cnpnei  15243  cnntr  15249  cncnp  15254  lmtopcnp  15274  txdis1cn  15302  xmettxlem  15533  metcnp3  15535  fsumcncntop  15591  cncfco  15615  mulcncf  15632  dedekindeulemuub  15641  dedekindeulemlu  15645  dedekindicclemuub  15650  dedekindicclemlu  15654  dedekindicclemicc  15656  ivthinclemlr  15661  ivthinclemur  15663  limcimo  15689  cnplimcim  15691  plymullem1  15772  plycolemc  15782  plycj  15785  dvply2g  15790  pilem3  15807  lgsfcl2  16039  lgsval2lem  16043  lgsdir  16068  lgsne0  16071  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  lgsquad3  16117  umgrvad2edg  16366  usgredg2vlem2  16378  wlkvtxiedg  16500  wlkvtxiedgg  16501  clwwlkccatlem  16555  eupth2lem3lem4fi  16628  eupth2lemsfi  16633  peano4nninf  16954  nnnninfex  16970  trilpolemeq1  16994