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  4028  tfr1onlemaccex  6406  tfrcllemaccex  6419  phplem4on  6928  dif1enen  6941  en2eqpr  6968  unsnfidcex  6981  unsnfidcel  6982  unfidisj  6983  undifdc  6985  fiintim  6992  ssfirab  6997  suplub2ti  7067  djudom  7159  omp1eomlem  7160  difinfsnlem  7165  difinfinf  7167  ctssdclemn0  7176  ctssdc  7179  nnnninfeq2  7195  nninfisol  7199  nninfwlpoimlemginf  7242  cc3  7335  ltaddpr  7664  ltexprlemrl  7677  addcanprleml  7681  addcanprlemu  7682  aptiprleml  7706  aptiprlemu  7707  cauappcvgprlemdisj  7718  cauappcvgprlemladdrl  7724  caucvgprlemloc  7742  caucvgprlemladdrl  7745  caucvgprprlemopl  7764  caucvgprprlemloc  7770  caucvgprprlemexbt  7773  suplocexprlemrl  7784  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemub  7790  caucvgsrlemoffres  7867  suplocsrlem  7875  axcaucvglemcau  7965  axcaucvglemres  7966  negf1o  8408  apreim  8630  apsym  8633  apcotr  8634  apadd1  8635  apneg  8638  mulext1  8639  mulge0  8646  apti  8649  aprcl  8673  qapne  9713  xaddf  9919  xaddval  9920  zsupcllemstep  10319  qtri3or  10330  exbtwnzlemstep  10337  rebtwn2zlemstep  10342  addmodlteq  10490  seq3f1olemqsumk  10604  seq3f1oleml  10608  qsqeqor  10742  apexp1  10810  faclbnd  10833  hashennnuni  10871  cvg1nlemres  11150  resqrexlemoverl  11186  resqrexlemglsq  11187  resqrexlemga  11188  minmax  11395  xrmaxleim  11409  xrmaxifle  11411  xrmaxiflemab  11412  xrmaxiflemlub  11413  xrmaxiflemcom  11414  xrmaxltsup  11423  xrmaxadd  11426  xrminmax  11430  xrbdtri  11441  climrecvg1n  11513  serf0  11517  zsumdc  11549  isumss  11556  fisumss  11557  fsum3cvg3  11561  fsumcl2lem  11563  fsumadd  11571  fsummulc2  11613  divcnv  11662  cvgratz  11697  mertenslem2  11701  zproddc  11744  fprodssdc  11755  fprodmul  11756  fprodsplitdc  11761  fprodcl2lem  11770  fprodle  11805  fprodmodd  11806  p1modz1  11959  dvds2ln  11989  divalglemeunn  12086  divalglemeuneg  12088  bitsfzolem  12118  dvdsbnd  12123  bezoutlemnewy  12163  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlembi  12172  dfgcd3  12177  uzwodc  12204  nninfctlemfo  12207  lcmgcdlem  12245  cncongr1  12271  cncongr2  12272  isprm5  12310  odzdvds  12414  pclemdc  12457  pceu  12464  dvdsprmpweqle  12506  pcadd  12509  1arith  12536  4sqexercise2  12568  4sqlem13m  12572  ennnfonelemhom  12632  ennnfonelemrnh  12633  ctinfomlemom  12644  resmhm2b  13121  mhmid  13245  mhmmnd  13246  ghmgrp  13248  mulgfng  13254  conjnmzb  13410  imasabl  13466  issrg  13521  ringinvnzdiv  13606  znunit  14215  psrval  14220  cnpnei  14455  cnntr  14461  cncnp  14466  lmtopcnp  14486  txdis1cn  14514  xmettxlem  14745  metcnp3  14747  fsumcncntop  14803  cncfco  14827  mulcncf  14844  dedekindeulemuub  14853  dedekindeulemlu  14857  dedekindicclemuub  14862  dedekindicclemlu  14866  dedekindicclemicc  14868  ivthinclemlr  14873  ivthinclemur  14875  limcimo  14901  cnplimcim  14903  plymullem1  14984  plycolemc  14994  plycj  14997  dvply2g  15002  pilem3  15019  lgsfcl2  15247  lgsval2lem  15251  lgsdir  15276  lgsne0  15279  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  lgsquad3  15325  peano4nninf  15650  trilpolemeq1  15684