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  8709  apreim  8931  apsym  8934  apcotr  8935  apadd1  8936  apneg  8939  mulext1  8940  mulge0  8947  apti  8950  aprcl  8974  qapne  10039  xaddf  10246  xaddval  10247  zsupcllemstep  10662  qtri3or  10675  exbtwnzlemstep  10682  rebtwn2zlemstep  10687  addmodlteq  10835  seq3f1olemqsumk  10949  seq3f1oleml  10953  qsqeqor  11087  apexp1  11156  faclbnd  11179  hashennnuni  11218  swrdswrd  11477  swrdccatin1  11497  pfxccatin12lem3  11504  swrdccat3blem  11511  cvg1nlemres  11751  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemga  11789  minmax  11996  xrmaxleim  12010  xrmaxifle  12012  xrmaxiflemab  12013  xrmaxiflemlub  12014  xrmaxiflemcom  12015  xrmaxltsup  12024  xrmaxadd  12027  xrminmax  12031  xrbdtri  12042  climrecvg1n  12114  serf0  12118  zsumdc  12151  isumss  12158  fisumss  12159  fsum3cvg3  12163  fsumcl2lem  12165  fsumadd  12173  fsummulc2  12215  divcnv  12264  cvgratz  12299  mertenslem2  12303  zproddc  12346  fprodssdc  12357  fprodmul  12358  fprodsplitdc  12363  fprodcl2lem  12372  fprodle  12407  fprodmodd  12408  p1modz1  12561  dvds2ln  12591  divalglemeunn  12688  divalglemeuneg  12690  bitsfzolem  12721  dvdsbnd  12733  bezoutlemnewy  12773  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlembi  12782  dfgcd3  12787  uzwodc  12814  nninfctlemfo  12817  lcmgcdlem  12855  cncongr1  12881  cncongr2  12882  isprm5  12920  odzdvds  13024  pclemdc  13067  pceu  13074  dvdsprmpweqle  13116  pcadd  13119  1arith  13146  4sqexercise2  13178  4sqlem13m  13182  ballotfilemcdc  13223  ballotfilemsle  13248  ennnfonelemhom  13306  ennnfonelemrnh  13307  ctinfomlemom  13318  resmhm2b  13796  mhmid  13918  mhmmnd  13919  ghmgrp  13921  mulgfng  13927  conjnmzb  14083  imasabl  14140  gsumvalfi  14152  gsumclfi  14159  gsummptfidmadd  14161  gsumsubmclfi  14163  gsumconstcmn  14166  prdsval  14173  issrg  14269  ringinvnzdiv  14355  znunit  14994  psrval  15050  mplsubgfilemcl  15090  cnpnei  15320  cnntr  15326  cncnp  15331  lmtopcnp  15351  txdis1cn  15379  xmettxlem  15610  metcnp3  15612  fsumcncntop  15668  cncfco  15692  mulcncf  15709  dedekindeulemuub  15718  dedekindeulemlu  15722  dedekindicclemuub  15727  dedekindicclemlu  15731  dedekindicclemicc  15733  ivthinclemlr  15738  ivthinclemur  15740  limcimo  15766  cnplimcim  15768  plymullem1  15849  plycolemc  15859  plycj  15862  dvply2g  15867  pilem3  15884  lgsfcl2  16125  lgsval2lem  16129  lgsdir  16154  lgsne0  16157  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  lgsquad3  16203  umgrvad2edg  16452  usgredg2vlem2  16464  wlkvtxiedg  16586  wlkvtxiedgg  16587  clwwlkccatlem  16641  eupth2lem3lem4fi  16714  eupth2lemsfi  16719  peano4nninf  17049  nnnninfex  17065  trilpolemeq1  17089