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  4000  tfr1onlemaccex  6351  tfrcllemaccex  6364  phplem4on  6869  dif1enen  6882  en2eqpr  6909  unsnfidcex  6921  unsnfidcel  6922  unfidisj  6923  undifdc  6925  fiintim  6930  ssfirab  6935  suplub2ti  7002  djudom  7094  omp1eomlem  7095  difinfsnlem  7100  difinfinf  7102  ctssdclemn0  7111  ctssdc  7114  nnnninfeq2  7129  nninfisol  7133  nninfwlpoimlemginf  7176  cc3  7269  ltaddpr  7598  ltexprlemrl  7611  addcanprleml  7615  addcanprlemu  7616  aptiprleml  7640  aptiprlemu  7641  cauappcvgprlemdisj  7652  cauappcvgprlemladdrl  7658  caucvgprlemloc  7676  caucvgprlemladdrl  7679  caucvgprprlemopl  7698  caucvgprprlemloc  7704  caucvgprprlemexbt  7707  suplocexprlemrl  7718  suplocexprlemru  7720  suplocexprlemdisj  7721  suplocexprlemloc  7722  suplocexprlemub  7724  caucvgsrlemoffres  7801  suplocsrlem  7809  axcaucvglemcau  7899  axcaucvglemres  7900  negf1o  8341  apreim  8562  apsym  8565  apcotr  8566  apadd1  8567  apneg  8570  mulext1  8571  mulge0  8578  apti  8581  aprcl  8605  qapne  9641  xaddf  9846  xaddval  9847  qtri3or  10245  exbtwnzlemstep  10250  rebtwn2zlemstep  10255  addmodlteq  10400  seq3f1olemqsumk  10501  seq3f1oleml  10505  qsqeqor  10633  apexp1  10700  faclbnd  10723  hashennnuni  10761  cvg1nlemres  10996  resqrexlemoverl  11032  resqrexlemglsq  11033  resqrexlemga  11034  minmax  11240  xrmaxleim  11254  xrmaxifle  11256  xrmaxiflemab  11257  xrmaxiflemlub  11258  xrmaxiflemcom  11259  xrmaxltsup  11268  xrmaxadd  11271  xrminmax  11275  xrbdtri  11286  climrecvg1n  11358  serf0  11362  zsumdc  11394  isumss  11401  fisumss  11402  fsum3cvg3  11406  fsumcl2lem  11408  fsumadd  11416  fsummulc2  11458  divcnv  11507  cvgratz  11542  mertenslem2  11546  zproddc  11589  fprodssdc  11600  fprodmul  11601  fprodsplitdc  11606  fprodcl2lem  11615  fprodle  11650  fprodmodd  11651  p1modz1  11803  dvds2ln  11833  divalglemeunn  11928  divalglemeuneg  11930  zsupcllemstep  11948  dvdsbnd  11959  bezoutlemnewy  11999  bezoutlemstep  12000  bezoutlemmain  12001  bezoutlembi  12008  dfgcd3  12013  uzwodc  12040  lcmgcdlem  12079  cncongr1  12105  cncongr2  12106  isprm5  12144  odzdvds  12247  pclemdc  12290  pceu  12297  dvdsprmpweqle  12338  pcadd  12341  1arith  12367  ennnfonelemhom  12418  ennnfonelemrnh  12419  ctinfomlemom  12430  mhmid  12984  mhmmnd  12985  ghmgrp  12987  mulgfng  12992  issrg  13153  ringinvnzdiv  13232  cnpnei  13758  cnntr  13764  cncnp  13769  lmtopcnp  13789  txdis1cn  13817  xmettxlem  14048  metcnp3  14050  fsumcncntop  14095  cncfco  14117  mulcncf  14130  dedekindeulemuub  14134  dedekindeulemlu  14138  dedekindicclemuub  14143  dedekindicclemlu  14147  dedekindicclemicc  14149  ivthinclemlr  14154  ivthinclemur  14156  limcimo  14173  cnplimcim  14175  pilem3  14243  lgsfcl2  14446  lgsval2lem  14450  lgsdir  14475  lgsne0  14478  peano4nninf  14794  trilpolemeq1  14827