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  6623  tfrcllemaccex  6636  phplem4on  7173  dif1enen  7188  elssdc  7213  en2eqpr  7218  unsnfidcex  7231  unsnfidcel  7232  unfidisj  7233  undifdc  7235  fiintim  7242  ssfirab  7248  suplub2ti  7347  djudom  7439  omp1eomlem  7440  difinfsnlem  7445  difinfinf  7447  ctssdclemn0  7456  ctssdc  7459  nnnninfeq2  7475  nninfisol  7479  nninfwlpoimlemginf  7522  cc3  7640  ltaddpr  7970  ltexprlemrl  7983  addcanprleml  7987  addcanprlemu  7988  aptiprleml  8012  aptiprlemu  8013  cauappcvgprlemdisj  8024  cauappcvgprlemladdrl  8030  caucvgprlemloc  8048  caucvgprlemladdrl  8051  caucvgprprlemopl  8070  caucvgprprlemloc  8076  caucvgprprlemexbt  8079  suplocexprlemrl  8090  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  caucvgsrlemoffres  8173  suplocsrlem  8181  axcaucvglemcau  8271  axcaucvglemres  8272  negf1o  8716  apreim  8939  apsym  8942  apcotr  8943  apadd1  8944  apneg  8947  mulext1  8948  mulge0  8955  apti  8958  aprcl  8982  qapne  10055  xaddf  10263  xaddval  10264  zsupcllemstep  10679  qtri3or  10692  exbtwnzlemstep  10699  rebtwn2zlemstep  10704  addmodlteq  10856  seq3f1olemqsumk  10970  seq3f1oleml  10974  qsqeqor  11108  apexp1  11178  faclbnd  11201  hashennnuni  11240  swrdswrd  11499  swrdccatin1  11519  pfxccatin12lem3  11526  swrdccat3blem  11533  cvg1nlemres  11773  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemga  11811  fiidxsupcl  12018  minmax  12020  xrmaxleim  12035  xrmaxifle  12037  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxiflemcom  12040  xrmaxltsup  12049  xrmaxadd  12052  xrminmax  12056  xrbdtri  12067  climrecvg1n  12139  serf0  12143  zsumdc  12176  isumss  12183  fisumss  12184  fsum3cvg3  12188  fsumcl2lem  12190  fsumadd  12198  fsummulc2  12240  divcnv  12289  cvgratz  12324  mertenslem2  12328  zproddc  12371  fprodssdc  12382  fprodmul  12383  fprodsplitdc  12388  fprodcl2lem  12397  fprodle  12432  fprodmodd  12433  p1modz1  12586  dvds2ln  12616  divalglemeunn  12713  divalglemeuneg  12715  bitsfzolem  12746  dvdsbnd  12758  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlembi  12807  dfgcd3  12812  uzwodc  12839  nninfctlemfo  12842  lcmgcdlem  12880  cncongr1  12906  cncongr2  12907  isprm5  12946  sqrtrirr  13014  odzdvds  13053  pclemdc  13096  pceu  13103  dvdsprmpweqle  13145  pcadd  13148  1arith  13175  4sqexercise2  13207  4sqlem13m  13211  ballotfilemcdc  13281  ballotfilemsle  13306  ennnfonelemhom  13364  ennnfonelemrnh  13365  ctinfomlemom  13376  resmhm2b  13855  mhmid  13977  mhmmnd  13978  ghmgrp  13980  mulgfng  13986  conjnmzb  14142  imasabl  14230  gsumvalfi  14242  gsumclfi  14249  gsummptfidmadd  14251  gsumsubmclfi  14253  gsummptfidmsplit  14254  gsumconstcmn  14266  prdsval  14280  issrg  14376  ringinvnzdiv  14462  znunit  15103  psrval  15159  psrbaglefifi  15172  psrass1fi  15201  psrdifi  15202  psrdirfi  15203  mplsubgfilemcl  15215  cnpnei  15445  cnntr  15451  cncnp  15456  lmtopcnp  15476  txdis1cn  15504  xmettxlem  15735  metcnp3  15737  fsumcncntop  15793  cncfco  15817  mulcncf  15834  dedekindeulemuub  15843  dedekindeulemlu  15847  dedekindicclemuub  15852  dedekindicclemlu  15856  dedekindicclemicc  15858  ivthinclemlr  15863  ivthinclemur  15865  limcimo  15891  cnplimcim  15893  plymullem1  15974  plycolemc  15984  plycj  15987  dvply2g  15992  pilem3  16010  lgsfcl2  16330  lgsval2lem  16334  lgsdir  16359  lgsne0  16362  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  lgsquad3  16408  umgrvad2edg  16657  usgredg2vlem2  16669  wlkvtxiedg  16791  wlkvtxiedgg  16792  clwwlkccatlem  16846  eupth2lem3lem4fi  16919  eupth2lemsfi  16924  peano4nninf  17255  nnnninfex  17271  trilpolemeq1  17296