Theorem ad2antrr 475

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad2antrr	|- ( ( ( ph /\ ch ) /\ th ) -> ps )

Proof of Theorem ad2antrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 272	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantlr 464	1 |- ( ( ( ph /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad3antrrr  479  simpll  499  simplll  503  simpllr  504  vtoclgft  2691  reupick  3307  euotd  4114  frirrg  4210  ralxfrd  4321  nnsucpred  4468  foun  5320  f1oprg  5343  dffo4  5500  foeqcnvco  5623  fliftfun  5629  isotr  5649  riotass2  5688  ovmpodxf  5828  mpoxopoveq  6067  tfrlem1  6135  tfrlemibacc  6153  tfrlemibfn  6155  tfrlemi14d  6160  tfrexlem  6161  tfr1onlembacc  6169  tfr1onlembfn  6171  tfr1onlemres  6176  tfrcllembacc  6182  tfrcllembfn  6184  tfrcllemres  6189  frecabcl  6226  nnmordi  6342  eroprf  6452  f1imaen2g  6617  xpen  6668  mapen  6669  mapdom1g  6670  mapxpen  6671  xpmapenlem  6672  phplem4dom  6685  nndomo  6687  phpm  6688  fidifsnen  6693  dif1enen  6703  fisbth  6706  fimax2gtrilemstep  6723  fimax2gtri  6724  en2eqpr  6730  unsnfidcex  6737  unsnfidcel  6738  ssfirab  6750  fidcenumlemrks  6769  sbthlemi8  6780  ordiso2  6835  updjud  6882  difinfsnlem  6899  ctssdclemn0  6910  ctssdclemr  6911  ctssdc  6912  enumctlemm  6913  enumct  6914  enomnilem  6922  fodju0  6931  exmidfodomrlemim  6966  dfplpq2  7063  nqpi  7087  nqnq0pi  7147  nq0nn  7151  elinp  7183  elnp1st2nd  7185  genprndl  7230  genprndu  7231  addnqprllem  7236  addnqprulem  7237  addnqprl  7238  addnqpru  7239  addlocpr  7245  nqprloc  7254  prmuloc  7275  mulnqprl  7277  mulnqpru  7278  mullocpr  7280  distrlem1prl  7291  distrlem1pru  7292  ltsopr  7305  ltexprlemopl  7310  ltexprlemopu  7312  ltexprlemloc  7316  ltexprlemrl  7319  ltexprlemru  7321  addcanprleml  7323  addcanprlemu  7324  recexprlemloc  7340  recexprlem1ssl  7342  recexprlem1ssu  7343  aptiprleml  7348  aptiprlemu  7349  archpr  7352  cauappcvgprlemm  7354  cauappcvgprlemopl  7355  cauappcvgprlemlol  7356  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  cauappcvgprlemladdru  7365  archrecpr  7373  caucvgprlemnkj  7375  caucvgprlemm  7377  caucvgprlemopl  7378  caucvgprlemlol  7379  caucvgprlemdisj  7383  caucvgprlemloc  7384  caucvgprlemladdfu  7386  caucvgprprlemnkltj  7398  caucvgprprlemnkeqj  7399  caucvgprprlemnjltk  7400  caucvgprprlemml  7403  caucvgprprlemopl  7406  caucvgprprlemlol  7407  caucvgprprlemdisj  7411  caucvgprprlemexbt  7415  caucvgprprlemexb  7416  caucvgprprlemaddq  7417  mulgt0sr  7473  caucvgsrlemcau  7488  caucvgsrlemoffcau  7493  caucvgsrlemoffres  7495  axcaucvglemcau  7583  axcaucvglemres  7584  cnegexlem1  7808  cnegex  7811  apsym  8234  apcotr  8235  apadd1  8236  mulext1  8240  mulge0  8247  apti  8250  conjmulap  8350  lemulge11  8482  creui  8576  nndiv  8619  zaddcllemneg  8945  suprzclex  9001  eluzuzle  9184  divfnzn  9263  qapne  9281  xrltso  9423  xrre  9444  xrre3  9446  xaddf  9468  xaddval  9469  xpncan  9495  xleadd1a  9497  xltadd1  9500  xleaddadd  9511  ixxss12  9530  elioc2  9560  elico2  9561  elicc2  9562  fzm1  9721  fzneuz  9722  eluzgtdifelfzo  9815  elfzonelfzo  9848  exfzdc  9858  qtri3or  9861  exbtwnzlemstep  9866  exbtwnzlemex  9868  exbtwnz  9869  modqid  9963  modqcyc2  9974  modqmuladd  9980  modqmuladdnn0  9982  modaddmodlo  10002  addmodlteq  10012  frecuzrdgrrn  10022  frec2uzrdg  10023  frecuzrdgsuc  10028  frecuzrdgsuctlem  10037  seq3clss  10081  iseqf1olemqcl  10100  iseqf1olemnab  10102  iseqf1olemab  10103  iseqf1olemmo  10106  iseqf1olemqf1o  10107  iseqf1olemjpcl  10109  iseqf1olemqpcl  10110  seq3f1olemqsumk  10113  seq3f1olemqsum  10114  seq3f1olemp  10116  seq3f1oleml  10117  seq3f1o  10118  seq3id3  10121  ser3ge0  10131  exp3val  10136  expap0  10164  facndiv  10326  faclbnd  10328  bcval5  10350  hashunlem  10391  hashun  10392  hashprg  10395  fiprsshashgt1  10404  hashfacen  10420  zfz1isolemiso  10423  zfz1isolem1  10424  seq3coll  10426  ovshftex  10432  2shfti  10444  seq3shft  10451  cjap  10519  caucvgrelemcau  10592  cvg1nlemcau  10596  cvg1nlemres  10597  recvguniq  10607  resqrexlemdecn  10624  resqrexlemcalc3  10628  resqrexlemcvg  10631  resqrexlemoverl  10633  leabs  10686  absexpzap  10692  ltabs  10699  abslt  10700  absle  10701  maxleim  10817  maxabslemval  10820  fimaxre2  10837  minmax  10840  xrmaxiflemcl  10853  xrmaxifle  10854  xrmaxiflemab  10855  xrmaxiflemlub  10856  xrmaxiflemcom  10857  xrmaxltsup  10866  xrmaxadd  10869  xrminmax  10873  xrbdtri  10884  2clim  10909  climshftlemg  10910  climsqz  10943  climsqz2  10944  climrecvg1n  10956  climcvg1nlem  10957  serf0  10960  sumrbdclem  10984  fsum3cvg  10985  summodclem3  10988  summodclem2a  10989  summodclem2  10990  zsumdc  10992  fsum3  10995  isumss  10999  fisumss  11000  fsum3cvg3  11004  fsumcl2lem  11006  fsumadd  11014  fsumsplit  11015  sumsnf  11017  fsum2d  11043  fisum0diag2  11055  fsummulc2  11056  modfsummod  11066  fsumabs  11073  fsumrelem  11079  fsumiun  11085  geoisumr  11126  cvgratnnlemseq  11134  cvgratz  11140  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  efcj  11177  efaddlem  11178  tanaddaplem  11243  nndivides  11295  dvdsext  11348  divalglemeunn  11413  divalglemex  11414  divalglemeuneg  11415  zsupcllemstep  11433  infssuzex  11437  dvdsbnd  11440  bezoutlemnewy  11477  bezoutlemstep  11478  bezoutlemmain  11479  bezoutlemzz  11483  bezoutlemaz  11484  bezoutlembz  11485  bezoutlemeu  11488  bezoutlemle  11489  bezoutlemsup  11490  dfgcd3  11491  dfgcd2  11495  bezoutr1  11514  dvdslcm  11543  lcmgcdlem  11551  qredeq  11570  qredeu  11571  divgcdcoprm0  11575  divgcdcoprmex  11576  cncongr1  11577  isprm2lem  11590  prmind2  11594  exprmfct  11611  prmdvdsfz  11612  prmexpb  11622  rpexp1i  11625  sqrt2irr  11633  sqne2sq  11647  nonsq  11677  phiprmpw  11690  hashgcdeq  11696  ennnfonelemg  11708  ennnfoneleminc  11716  ennnfonelemkh  11717  ennnfonelemhf1o  11718  ennnfonelemex  11719  ennnfonelemhom  11720  ennnfonelemfun  11722  ennnfonelemf1  11723  ennnfonelemrn  11724  ennnfonelemdm  11725  ennnfonelemnn0  11727  ennnfonelemim  11729  exmidunben  11731  ctinfomlemom  11732  ctinf  11735  isstruct2r  11752  tgdom  12023  neipsm  12105  tgrest  12120  cnfval  12145  cnpfval  12146  cnpval  12148  iscnp4  12168  cnpnei  12169  cnptopco  12172  cncnpi  12178  cncnp  12180  cnptopresti  12188  cnptoprest2  12190  cndis  12191  lmtopcnp  12200  txbasval  12217  neitx  12218  txcnp  12221  txcnmpt  12223  txcn  12225  imasnopn  12249  psmetres2  12261  isxmet2d  12276  xblss2ps  12332  xblss2  12333  blbas  12361  neibl  12419  metss2lem  12425  metrest  12434  metcnp3  12435  metcnp  12436  metcnp2  12437  metcnpi  12439  metcnpi2  12440  mulc1cncf  12489  cncfco  12491  mulcncflem  12502  mulcncf  12503  limcimolemlt  12513  bj-findis  12762  pwle2  12779  pwf1oexmid  12780  nnsf  12783  peano4nninf  12784  nninfalllemn  12786  nninfall  12788  nninfsellemeq  12794  nninfsellemeqinf  12796  qdencn  12806  refeq  12807  trilpolemeq1  12817  trilpolemlt1  12818