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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad4antr  498  ad5ant12  522  disjiun  4125  tfr1onlemaccex  6619  tfrcllemaccex  6632  phplem4on  7169  dif1enen  7184  elssdc  7209  en2eqpr  7214  unsnfidcex  7227  unsnfidcel  7228  unfidisj  7229  undifdc  7231  fiintim  7238  ssfirab  7244  suplub2ti  7341  djudom  7433  omp1eomlem  7434  difinfsnlem  7439  difinfinf  7441  ctssdclemn0  7450  ctssdc  7453  nnnninfeq2  7469  nninfisol  7473  nninfwlpoimlemginf  7516  cc3  7634  ltaddpr  7964  ltexprlemrl  7977  addcanprleml  7981  addcanprlemu  7982  aptiprleml  8006  aptiprlemu  8007  cauappcvgprlemdisj  8018  cauappcvgprlemladdrl  8024  caucvgprlemloc  8042  caucvgprlemladdrl  8045  caucvgprprlemopl  8064  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  suplocexprlemrl  8084  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  caucvgsrlemoffres  8167  suplocsrlem  8175  axcaucvglemcau  8265  axcaucvglemres  8266  negf1o  8710  apreim  8933  apsym  8936  apcotr  8937  apadd1  8938  apneg  8941  mulext1  8942  mulge0  8949  apti  8952  aprcl  8976  qapne  10048  xaddf  10256  xaddval  10257  zsupcllemstep  10672  qtri3or  10685  exbtwnzlemstep  10692  rebtwn2zlemstep  10697  addmodlteq  10848  seq3f1olemqsumk  10962  seq3f1oleml  10966  qsqeqor  11100  apexp1  11170  faclbnd  11193  hashennnuni  11232  swrdswrd  11491  swrdccatin1  11511  pfxccatin12lem3  11518  swrdccat3blem  11525  cvg1nlemres  11765  resqrexlemoverl  11801  resqrexlemglsq  11802  resqrexlemga  11803  minmax  12011  xrmaxleim  12026  xrmaxifle  12028  xrmaxiflemab  12029  xrmaxiflemlub  12030  xrmaxiflemcom  12031  xrmaxltsup  12040  xrmaxadd  12043  xrminmax  12047  xrbdtri  12058  climrecvg1n  12130  serf0  12134  zsumdc  12167  isumss  12174  fisumss  12175  fsum3cvg3  12179  fsumcl2lem  12181  fsumadd  12189  fsummulc2  12231  divcnv  12280  cvgratz  12315  mertenslem2  12319  zproddc  12362  fprodssdc  12373  fprodmul  12374  fprodsplitdc  12379  fprodcl2lem  12388  fprodle  12423  fprodmodd  12424  p1modz1  12577  dvds2ln  12607  divalglemeunn  12704  divalglemeuneg  12706  bitsfzolem  12737  dvdsbnd  12749  bezoutlemnewy  12789  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlembi  12798  dfgcd3  12803  uzwodc  12830  nninfctlemfo  12833  lcmgcdlem  12871  cncongr1  12897  cncongr2  12898  isprm5  12937  sqrtrirr  13005  odzdvds  13044  pclemdc  13087  pceu  13094  dvdsprmpweqle  13136  pcadd  13139  1arith  13166  4sqexercise2  13198  4sqlem13m  13202  ballotfilemcdc  13272  ballotfilemsle  13297  ennnfonelemhom  13355  ennnfonelemrnh  13356  ctinfomlemom  13367  resmhm2b  13845  mhmid  13967  mhmmnd  13968  ghmgrp  13970  mulgfng  13976  conjnmzb  14132  imasabl  14189  gsumvalfi  14201  gsumclfi  14208  gsummptfidmadd  14210  gsumsubmclfi  14212  gsumconstcmn  14215  prdsval  14222  issrg  14318  ringinvnzdiv  14404  znunit  15043  psrval  15099  mplsubgfilemcl  15139  cnpnei  15369  cnntr  15375  cncnp  15380  lmtopcnp  15400  txdis1cn  15428  xmettxlem  15659  metcnp3  15661  fsumcncntop  15717  cncfco  15741  mulcncf  15758  dedekindeulemuub  15767  dedekindeulemlu  15771  dedekindicclemuub  15776  dedekindicclemlu  15780  dedekindicclemicc  15782  ivthinclemlr  15787  ivthinclemur  15789  limcimo  15815  cnplimcim  15817  plymullem1  15898  plycolemc  15908  plycj  15911  dvply2g  15916  pilem3  15934  lgsfcl2  16223  lgsval2lem  16227  lgsdir  16252  lgsne0  16255  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  lgsquad3  16301  umgrvad2edg  16550  usgredg2vlem2  16562  wlkvtxiedg  16684  wlkvtxiedgg  16685  clwwlkccatlem  16739  eupth2lem3lem4fi  16812  eupth2lemsfi  16817  peano4nninf  17147  nnnninfex  17163  trilpolemeq1  17187