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  4078  tfr1onlemaccex  6494  tfrcllemaccex  6507  phplem4on  7029  dif1enen  7042  en2eqpr  7069  unsnfidcex  7082  unsnfidcel  7083  unfidisj  7084  undifdc  7086  fiintim  7093  ssfirab  7098  suplub2ti  7168  djudom  7260  omp1eomlem  7261  difinfsnlem  7266  difinfinf  7268  ctssdclemn0  7277  ctssdc  7280  nnnninfeq2  7296  nninfisol  7300  nninfwlpoimlemginf  7343  cc3  7454  ltaddpr  7784  ltexprlemrl  7797  addcanprleml  7801  addcanprlemu  7802  aptiprleml  7826  aptiprlemu  7827  cauappcvgprlemdisj  7838  cauappcvgprlemladdrl  7844  caucvgprlemloc  7862  caucvgprlemladdrl  7865  caucvgprprlemopl  7884  caucvgprprlemloc  7890  caucvgprprlemexbt  7893  suplocexprlemrl  7904  suplocexprlemru  7906  suplocexprlemdisj  7907  suplocexprlemloc  7908  suplocexprlemub  7910  caucvgsrlemoffres  7987  suplocsrlem  7995  axcaucvglemcau  8085  axcaucvglemres  8086  negf1o  8528  apreim  8750  apsym  8753  apcotr  8754  apadd1  8755  apneg  8758  mulext1  8759  mulge0  8766  apti  8769  aprcl  8793  qapne  9834  xaddf  10040  xaddval  10041  zsupcllemstep  10449  qtri3or  10460  exbtwnzlemstep  10467  rebtwn2zlemstep  10472  addmodlteq  10620  seq3f1olemqsumk  10734  seq3f1oleml  10738  qsqeqor  10872  apexp1  10940  faclbnd  10963  hashennnuni  11001  swrdswrd  11237  swrdccatin1  11257  pfxccatin12lem3  11264  swrdccat3blem  11271  cvg1nlemres  11496  resqrexlemoverl  11532  resqrexlemglsq  11533  resqrexlemga  11534  minmax  11741  xrmaxleim  11755  xrmaxifle  11757  xrmaxiflemab  11758  xrmaxiflemlub  11759  xrmaxiflemcom  11760  xrmaxltsup  11769  xrmaxadd  11772  xrminmax  11776  xrbdtri  11787  climrecvg1n  11859  serf0  11863  zsumdc  11895  isumss  11902  fisumss  11903  fsum3cvg3  11907  fsumcl2lem  11909  fsumadd  11917  fsummulc2  11959  divcnv  12008  cvgratz  12043  mertenslem2  12047  zproddc  12090  fprodssdc  12101  fprodmul  12102  fprodsplitdc  12107  fprodcl2lem  12116  fprodle  12151  fprodmodd  12152  p1modz1  12305  dvds2ln  12335  divalglemeunn  12432  divalglemeuneg  12434  bitsfzolem  12465  dvdsbnd  12477  bezoutlemnewy  12517  bezoutlemstep  12518  bezoutlemmain  12519  bezoutlembi  12526  dfgcd3  12531  uzwodc  12558  nninfctlemfo  12561  lcmgcdlem  12599  cncongr1  12625  cncongr2  12626  isprm5  12664  odzdvds  12768  pclemdc  12811  pceu  12818  dvdsprmpweqle  12860  pcadd  12863  1arith  12890  4sqexercise2  12922  4sqlem13m  12926  ennnfonelemhom  12986  ennnfonelemrnh  12987  ctinfomlemom  12998  prdsval  13306  resmhm2b  13522  mhmid  13652  mhmmnd  13653  ghmgrp  13655  mulgfng  13661  conjnmzb  13817  imasabl  13873  issrg  13928  ringinvnzdiv  14013  znunit  14623  psrval  14630  mplsubgfilemcl  14663  cnpnei  14893  cnntr  14899  cncnp  14904  lmtopcnp  14924  txdis1cn  14952  xmettxlem  15183  metcnp3  15185  fsumcncntop  15241  cncfco  15265  mulcncf  15282  dedekindeulemuub  15291  dedekindeulemlu  15295  dedekindicclemuub  15300  dedekindicclemlu  15304  dedekindicclemicc  15306  ivthinclemlr  15311  ivthinclemur  15313  limcimo  15339  cnplimcim  15341  plymullem1  15422  plycolemc  15432  plycj  15435  dvply2g  15440  pilem3  15457  lgsfcl2  15685  lgsval2lem  15689  lgsdir  15714  lgsne0  15717  gausslemma2dlem1a  15737  gausslemma2dlem1f1o  15739  lgsquad3  15763  umgrvad2edg  16009  usgredg2vlem2  16021  wlkvtxiedg  16056  wlkvtxiedgg  16057  peano4nninf  16372  nnnninfex  16388  trilpolemeq1  16408