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  6624  tfrcllemaccex  6637  phplem4on  7175  dif1enen  7190  elssdc  7215  en2eqpr  7220  unsnfidcex  7233  unsnfidcel  7234  unfidisj  7235  undifdc  7237  fiintim  7244  ssfirab  7250  funisfsuppdc  7298  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  10054  xaddf  10262  xaddval  10263  zsupcllemstep  10678  qtri3or  10691  exbtwnzlemstep  10698  rebtwn2zlemstep  10703  addmodlteq  10855  seq3f1olemqsumk  10969  seq3f1oleml  10973  qsqeqor  11107  apexp1  11177  faclbnd  11200  hashennnuni  11239  swrdswrd  11498  swrdccatin1  11518  pfxccatin12lem3  11525  swrdccat3blem  11532  cvg1nlemres  11772  resqrexlemoverl  11808  resqrexlemglsq  11809  resqrexlemga  11810  fiidxsupcl  12017  minmax  12019  xrmaxleim  12034  xrmaxifle  12036  xrmaxiflemab  12037  xrmaxiflemlub  12038  xrmaxiflemcom  12039  xrmaxltsup  12048  xrmaxadd  12051  xrminmax  12055  xrbdtri  12066  climrecvg1n  12138  serf0  12142  zsumdc  12175  isumss  12182  fisumss  12183  fsum3cvg3  12187  fsumcl2lem  12189  fsumadd  12197  fsummulc2  12239  divcnv  12288  cvgratz  12323  mertenslem2  12327  zproddc  12370  fprodssdc  12381  fprodmul  12382  fprodsplitdc  12387  fprodcl2lem  12396  fprodle  12431  fprodmodd  12432  p1modz1  12585  dvds2ln  12615  divalglemeunn  12712  divalglemeuneg  12714  bitsfzolem  12745  dvdsbnd  12757  bezoutlemnewy  12797  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlembi  12806  dfgcd3  12811  uzwodc  12838  nninfctlemfo  12841  lcmgcdlem  12879  cncongr1  12905  cncongr2  12906  isprm5  12945  sqrtrirr  13013  odzdvds  13052  pclemdc  13095  pceu  13102  dvdsprmpweqle  13144  pcadd  13147  1arith  13174  4sqexercise2  13206  4sqlem13m  13210  ballotfilemcdc  13280  ballotfilemsle  13305  ennnfonelemhom  13363  ennnfonelemrnh  13364  ctinfomlemom  13375  resmhm2b  13854  mhmid  13976  mhmmnd  13977  ghmgrp  13979  mulgfng  13985  conjnmzb  14141  imasabl  14229  gsumvalfi  14241  gsumclfi  14248  gsummptfidmadd  14250  gsumsubmclfi  14252  gsummptfidmsplit  14253  gsumconstcmn  14265  prdsval  14279  issrg  14375  ringinvnzdiv  14461  znunit  15102  psrval  15160  psrbaglefifi  15175  psrbagmaxlem1  15178  psrass1fi  15210  psrdifi  15211  psrdirfi  15212  mplsubgfilemcl  15232  mplsubgfileminv  15233  cnpnei  15462  cnntr  15468  cncnp  15473  lmtopcnp  15493  txdis1cn  15521  xmettxlem  15752  metcnp3  15754  fsumcncntop  15810  cncfco  15834  mulcncf  15851  dedekindeulemuub  15860  dedekindeulemlu  15864  dedekindicclemuub  15869  dedekindicclemlu  15873  dedekindicclemicc  15875  ivthinclemlr  15880  ivthinclemur  15882  limcimo  15908  cnplimcim  15910  plymullem1  15991  plycolemc  16001  plycj  16004  dvply2g  16009  pilem3  16027  lgsfcl2  16347  lgsval2lem  16351  lgsdir  16376  lgsne0  16379  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  lgsquad3  16425  umgrvad2edg  16674  usgredg2vlem2  16686  wlkvtxiedg  16808  wlkvtxiedgg  16809  clwwlkccatlem  16863  eupth2lem3lem4fi  16936  eupth2lemsfi  16941  peano4nninf  17272  nnnninfex  17288  trilpolemeq1  17313