ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad2antrr Unicode version

Theorem ad2antrr 465
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
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantr 265 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantlr 454 1  |-  ( ( ( ph  /\  ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  ad3antrrr  469  simpll  489  simplll  493  simpllr  494  vtoclgft  2621  reupick  3249  euotd  4019  frirrg  4115  ralxfrd  4222  foun  5173  f1oprg  5196  dffo4  5343  foeqcnvco  5458  fliftfun  5464  isotr  5484  riotass2  5522  ovmpt2dxf  5654  mpt2xopoveq  5886  tfrlem1  5954  tfrlemibacc  5971  tfrlemibfn  5973  tfrlemi14d  5978  tfrexlem  5979  nnmordi  6120  eroprf  6230  f1imaen2g  6304  phplem4dom  6355  nndomo  6357  phpm  6358  fidifsnen  6362  fisbth  6371  ordiso2  6415  dfplpq2  6510  nqpi  6534  nqnq0pi  6594  nq0nn  6598  elinp  6630  elnp1st2nd  6632  genprndl  6677  genprndu  6678  addnqprllem  6683  addnqprulem  6684  addnqprl  6685  addnqpru  6686  addlocpr  6692  nqprloc  6701  prmuloc  6722  mulnqprl  6724  mulnqpru  6725  mullocpr  6727  distrlem1prl  6738  distrlem1pru  6739  ltsopr  6752  ltexprlemopl  6757  ltexprlemopu  6759  ltexprlemloc  6763  ltexprlemrl  6766  ltexprlemru  6768  addcanprleml  6770  addcanprlemu  6771  recexprlemloc  6787  recexprlem1ssl  6789  recexprlem1ssu  6790  aptiprleml  6795  aptiprlemu  6796  archpr  6799  cauappcvgprlemm  6801  cauappcvgprlemopl  6802  cauappcvgprlemlol  6803  cauappcvgprlemladdfu  6810  cauappcvgprlemladdfl  6811  cauappcvgprlemladdru  6812  archrecpr  6820  caucvgprlemnkj  6822  caucvgprlemm  6824  caucvgprlemopl  6825  caucvgprlemlol  6826  caucvgprlemdisj  6830  caucvgprlemloc  6831  caucvgprlemladdfu  6833  caucvgprprlemnkltj  6845  caucvgprprlemnkeqj  6846  caucvgprprlemnjltk  6847  caucvgprprlemml  6850  caucvgprprlemopl  6853  caucvgprprlemlol  6854  caucvgprprlemdisj  6858  caucvgprprlemexbt  6862  caucvgprprlemexb  6863  caucvgprprlemaddq  6864  mulgt0sr  6920  caucvgsrlemcau  6935  caucvgsrlemoffcau  6940  caucvgsrlemoffres  6942  axcaucvglemcau  7030  axcaucvglemres  7031  cnegexlem1  7249  cnegex  7252  apsym  7671  apcotr  7672  apadd1  7673  mulext1  7677  mulge0  7684  apti  7687  conjmulap  7780  lemulge11  7907  creui  7988  nndiv  8030  zaddcllemneg  8341  eluzuzle  8577  divfnzn  8653  qapne  8671  xrltso  8818  xrre  8834  xrre3  8836  ixxss12  8876  elioc2  8906  elico2  8907  elicc2  8908  fzm1  9064  fzneuz  9065  eluzgtdifelfzo  9155  elfzonelfzo  9188  qtri3or  9200  qbtwnzlemstep  9205  qbtwnzlemex  9207  qbtwnz  9208  modqid  9299  modqcyc2  9310  modqmuladd  9316  modqmuladdnn0  9318  modaddmodlo  9338  addmodlteq  9348  frecuzrdgrrn  9358  iseqid3s  9410  expival  9422  expap0  9450  facndiv  9607  faclbnd  9609  ibcval5  9631  ovshftex  9648  2shfti  9660  cjap  9734  caucvgrelemcau  9807  cvg1nlemcau  9811  cvg1nlemres  9812  recvguniq  9822  resqrexlemdecn  9839  resqrexlemcalc3  9843  resqrexlemcvg  9846  resqrexlemoverl  9848  leabs  9901  absexpzap  9907  ltabs  9914  abslt  9915  absle  9916  2clim  10053  climshftlemg  10054  climsqz  10086  climsqz2  10087  climrecvg1n  10098  climcvg1nlem  10099  serif0  10102  nndivides  10115  dvdsext  10167  divalglemeunn  10233  divalglemex  10234  divalglemeuneg  10235  sqrt2irr  10251  bj-findis  10491  qdencn  10511
  Copyright terms: Public domain W3C validator