Theorem ad3antrrr 492

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 488	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  494  ad5ant12  518  disjiun  3999  tfr1onlemaccex  6349  tfrcllemaccex  6362  phplem4on  6867  dif1enen  6880  en2eqpr  6907  unsnfidcex  6919  unsnfidcel  6920  unfidisj  6921  undifdc  6923  fiintim  6928  ssfirab  6933  suplub2ti  7000  djudom  7092  omp1eomlem  7093  difinfsnlem  7098  difinfinf  7100  ctssdclemn0  7109  ctssdc  7112  nnnninfeq2  7127  nninfisol  7131  nninfwlpoimlemginf  7174  cc3  7267  ltaddpr  7596  ltexprlemrl  7609  addcanprleml  7613  addcanprlemu  7614  aptiprleml  7638  aptiprlemu  7639  cauappcvgprlemdisj  7650  cauappcvgprlemladdrl  7656  caucvgprlemloc  7674  caucvgprlemladdrl  7677  caucvgprprlemopl  7696  caucvgprprlemloc  7702  caucvgprprlemexbt  7705  suplocexprlemrl  7716  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemub  7722  caucvgsrlemoffres  7799  suplocsrlem  7807  axcaucvglemcau  7897  axcaucvglemres  7898  negf1o  8339  apreim  8560  apsym  8563  apcotr  8564  apadd1  8565  apneg  8568  mulext1  8569  mulge0  8576  apti  8579  aprcl  8603  qapne  9639  xaddf  9844  xaddval  9845  qtri3or  10243  exbtwnzlemstep  10248  rebtwn2zlemstep  10253  addmodlteq  10398  seq3f1olemqsumk  10499  seq3f1oleml  10503  qsqeqor  10631  apexp1  10698  faclbnd  10721  hashennnuni  10759  cvg1nlemres  10994  resqrexlemoverl  11030  resqrexlemglsq  11031  resqrexlemga  11032  minmax  11238  xrmaxleim  11252  xrmaxifle  11254  xrmaxiflemab  11255  xrmaxiflemlub  11256  xrmaxiflemcom  11257  xrmaxltsup  11266  xrmaxadd  11269  xrminmax  11273  xrbdtri  11284  climrecvg1n  11356  serf0  11360  zsumdc  11392  isumss  11399  fisumss  11400  fsum3cvg3  11404  fsumcl2lem  11406  fsumadd  11414  fsummulc2  11456  divcnv  11505  cvgratz  11540  mertenslem2  11544  zproddc  11587  fprodssdc  11598  fprodmul  11599  fprodsplitdc  11604  fprodcl2lem  11613  fprodle  11648  fprodmodd  11649  p1modz1  11801  dvds2ln  11831  divalglemeunn  11926  divalglemeuneg  11928  zsupcllemstep  11946  dvdsbnd  11957  bezoutlemnewy  11997  bezoutlemstep  11998  bezoutlemmain  11999  bezoutlembi  12006  dfgcd3  12011  uzwodc  12038  lcmgcdlem  12077  cncongr1  12103  cncongr2  12104  isprm5  12142  odzdvds  12245  pclemdc  12288  pceu  12295  dvdsprmpweqle  12336  pcadd  12339  1arith  12365  ennnfonelemhom  12416  ennnfonelemrnh  12417  ctinfomlemom  12428  mhmid  12979  mhmmnd  12980  ghmgrp  12982  mulgfng  12987  issrg  13148  ringinvnzdiv  13227  cnpnei  13722  cnntr  13728  cncnp  13733  lmtopcnp  13753  txdis1cn  13781  xmettxlem  14012  metcnp3  14014  fsumcncntop  14059  cncfco  14081  mulcncf  14094  dedekindeulemuub  14098  dedekindeulemlu  14102  dedekindicclemuub  14107  dedekindicclemlu  14111  dedekindicclemicc  14113  ivthinclemlr  14118  ivthinclemur  14120  limcimo  14137  cnplimcim  14139  pilem3  14207  lgsfcl2  14410  lgsval2lem  14414  lgsdir  14439  lgsne0  14442  peano4nninf  14758  trilpolemeq1  14791