Theorem ad2antrr 472

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 270	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantlr 461	1 |- ( ( ( ph /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  ad3antrrr  476  simpll  496  simplll  500  simpllr  501  vtoclgft  2663  reupick  3272  euotd  4055  frirrg  4151  ralxfrd  4258  foun  5235  f1oprg  5258  dffo4  5410  foeqcnvco  5530  fliftfun  5536  isotr  5556  riotass2  5595  ovmpt2dxf  5727  mpt2xopoveq  5959  tfrlem1  6027  tfrlemibacc  6045  tfrlemibfn  6047  tfrlemi14d  6052  tfrexlem  6053  tfr1onlembacc  6061  tfr1onlembfn  6063  tfr1onlemres  6068  tfrcllembacc  6074  tfrcllembfn  6076  tfrcllemres  6081  frecabcl  6118  nnmordi  6227  eroprf  6337  f1imaen2g  6462  xpen  6513  mapen  6514  mapdom1g  6515  mapxpen  6516  xpmapenlem  6517  phplem4dom  6530  nndomo  6532  phpm  6533  fidifsnen  6538  dif1enen  6548  fisbth  6551  fimax2gtrilemstep  6568  fimax2gtri  6569  en2eqpr  6575  unsnfidcex  6582  unsnfidcel  6583  ssfirab  6593  sbthlemi8  6617  ordiso2  6672  updjud  6717  enomnilem  6738  fodjuomnilem0  6746  exmidfodomrlemim  6771  dfplpq2  6857  nqpi  6881  nqnq0pi  6941  nq0nn  6945  elinp  6977  elnp1st2nd  6979  genprndl  7024  genprndu  7025  addnqprllem  7030  addnqprulem  7031  addnqprl  7032  addnqpru  7033  addlocpr  7039  nqprloc  7048  prmuloc  7069  mulnqprl  7071  mulnqpru  7072  mullocpr  7074  distrlem1prl  7085  distrlem1pru  7086  ltsopr  7099  ltexprlemopl  7104  ltexprlemopu  7106  ltexprlemloc  7110  ltexprlemrl  7113  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  recexprlemloc  7134  recexprlem1ssl  7136  recexprlem1ssu  7137  aptiprleml  7142  aptiprlemu  7143  archpr  7146  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  archrecpr  7167  caucvgprlemnkj  7169  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemladdfu  7180  caucvgprprlemnkltj  7192  caucvgprprlemnkeqj  7193  caucvgprprlemnjltk  7194  caucvgprprlemml  7197  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemdisj  7205  caucvgprprlemexbt  7209  caucvgprprlemexb  7210  caucvgprprlemaddq  7211  mulgt0sr  7267  caucvgsrlemcau  7282  caucvgsrlemoffcau  7287  caucvgsrlemoffres  7289  axcaucvglemcau  7377  axcaucvglemres  7378  cnegexlem1  7601  cnegex  7604  apsym  8024  apcotr  8025  apadd1  8026  mulext1  8030  mulge0  8037  apti  8040  conjmulap  8135  lemulge11  8262  creui  8355  nndiv  8397  zaddcllemneg  8722  suprzclex  8777  eluzuzle  8959  divfnzn  9038  qapne  9056  xrltso  9198  xrre  9214  xrre3  9216  ixxss12  9256  elioc2  9286  elico2  9287  elicc2  9288  fzm1  9444  fzneuz  9445  eluzgtdifelfzo  9536  elfzonelfzo  9569  exfzdc  9579  qtri3or  9582  exbtwnzlemstep  9587  exbtwnzlemex  9589  exbtwnz  9590  modqid  9684  modqcyc2  9695  modqmuladd  9701  modqmuladdnn0  9703  modaddmodlo  9723  addmodlteq  9733  frecuzrdgrrn  9743  frec2uzrdg  9744  frecuzrdgsuc  9749  frecuzrdgsuctlem  9758  iseqclt  9798  iseqoveq  9799  iseqf1olemqcl  9820  iseqf1olemnab  9822  iseqf1olemab  9823  iseqf1olemmo  9826  iseqf1olemqf1o  9827  iseqf1olemjpcl  9829  iseqf1olemqpcl  9830  iseqf1olemqsumk  9833  iseqf1olemqsum  9834  iseqf1olemp  9836  iseqf1oleml  9837  iseqf1o  9838  iseqid3s  9842  expival  9856  expap0  9884  facndiv  10044  faclbnd  10046  ibcval5  10068  hashunlem  10109  hashun  10110  hashprg  10113  fiprsshashgt1  10122  hashfacen  10138  zfz1isolemiso  10141  zfz1isolem1  10142  iseqcoll  10144  ovshftex  10150  2shfti  10162  cjap  10236  caucvgrelemcau  10309  cvg1nlemcau  10313  cvg1nlemres  10314  recvguniq  10324  resqrexlemdecn  10341  resqrexlemcalc3  10345  resqrexlemcvg  10348  resqrexlemoverl  10350  leabs  10403  absexpzap  10409  ltabs  10416  abslt  10417  absle  10418  maxleim  10534  maxabslemval  10537  fimaxre2  10553  minmax  10556  2clim  10584  climshftlemg  10585  climsqz  10617  climsqz2  10618  climrecvg1n  10629  climcvg1nlem  10630  serif0  10633  isumrblem  10657  fisumcvg  10658  isummolem3  10661  isummolem2a  10662  isummolem2  10663  zisum  10665  fisum  10667  isumss  10671  fisumss  10672  fisumcvg3  10676  fsumcl2lem  10677  nndivides  10685  dvdsext  10738  divalglemeunn  10803  divalglemex  10804  divalglemeuneg  10805  zsupcllemstep  10823  infssuzex  10827  dvdsbnd  10830  bezoutlemnewy  10867  bezoutlemstep  10868  bezoutlemmain  10869  bezoutlemzz  10873  bezoutlemaz  10874  bezoutlembz  10875  bezoutlemeu  10878  bezoutlemle  10879  bezoutlemsup  10880  dfgcd3  10881  dfgcd2  10885  bezoutr1  10904  dvdslcm  10933  lcmgcdlem  10941  qredeq  10960  qredeu  10961  divgcdcoprm0  10965  divgcdcoprmex  10966  cncongr1  10967  isprm2lem  10980  prmind2  10984  exprmfct  11001  prmdvdsfz  11002  prmexpb  11012  rpexp1i  11015  sqrt2irr  11023  sqne2sq  11037  nonsq  11067  phiprmpw  11080  hashgcdeq  11086  bj-findis  11319  nnsucpred  11336  nnsf  11340  peano4nninf  11341  nninfalllemn  11343  nninfall  11345  nninfsellemeq  11351  nninfsellemeqinf  11353  qdencn  11360