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

Theorem ad2antrr 457
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 261 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantlr 446 1  |-  ( ( ( ph  /\  ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  ad3antrrr  461  simpll  481  simplll  485  simpllr  486  vtoclgft  2604  reupick  3221  euotd  3991  frirrg  4087  ralxfrd  4194  foun  5145  f1oprg  5168  dffo4  5315  foeqcnvco  5430  fliftfun  5436  isotr  5456  riotass2  5494  ovmpt2dxf  5626  mpt2xopoveq  5855  tfrlem1  5923  tfrlemibacc  5940  tfrlemibfn  5942  tfrlemi14d  5947  tfrexlem  5948  nnmordi  6089  eroprf  6199  f1imaen2g  6273  phplem4dom  6324  nndomo  6326  phpm  6327  fidifsnen  6331  fisbth  6340  ordiso2  6357  dfplpq2  6452  nqpi  6476  nqnq0pi  6536  nq0nn  6540  elinp  6572  elnp1st2nd  6574  genprndl  6619  genprndu  6620  addnqprllem  6625  addnqprulem  6626  addnqprl  6627  addnqpru  6628  addlocpr  6634  nqprloc  6643  prmuloc  6664  mulnqprl  6666  mulnqpru  6667  mullocpr  6669  distrlem1prl  6680  distrlem1pru  6681  ltsopr  6694  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemloc  6705  ltexprlemrl  6708  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  aptiprleml  6737  aptiprlemu  6738  archpr  6741  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  archrecpr  6762  caucvgprlemnkj  6764  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnjltk  6789  caucvgprprlemml  6792  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemdisj  6800  caucvgprprlemexbt  6804  caucvgprprlemexb  6805  caucvgprprlemaddq  6806  mulgt0sr  6862  caucvgsrlemcau  6877  caucvgsrlemoffcau  6882  caucvgsrlemoffres  6884  axcaucvglemcau  6972  axcaucvglemres  6973  cnegexlem1  7186  cnegex  7189  apsym  7597  apcotr  7598  apadd1  7599  mulext1  7603  mulge0  7610  apti  7613  conjmulap  7705  lemulge11  7832  creui  7912  nndiv  7954  zaddcllemneg  8284  eluzuzle  8481  divfnzn  8556  qapne  8574  xrltso  8717  xrre  8733  xrre3  8735  ixxss12  8775  elioc2  8805  elico2  8806  elicc2  8807  fzm1  8962  fzneuz  8963  eluzgtdifelfzo  9053  elfzonelfzo  9086  qtri3or  9098  qbtwnzlemstep  9103  qbtwnzlemex  9105  qbtwnz  9106  frecuzrdgrrn  9194  iseqid3s  9246  expival  9257  expap0  9285  ovshftex  9420  2shfti  9432  cjap  9506  caucvgrelemcau  9579  cvg1nlemcau  9583  cvg1nlemres  9584  recvguniq  9593  resqrexlemdecn  9610  resqrexlemcalc3  9614  resqrexlemcvg  9617  resqrexlemoverl  9619  leabs  9672  absexpzap  9676  ltabs  9683  abslt  9684  absle  9685  2clim  9822  climshftlemg  9823  climsqz  9855  climsqz2  9856  climrecvg1n  9867  climcvg1nlem  9868  serif0  9871  sqrt2irr  9878  bj-findis  10104  qdencn  10124
  Copyright terms: Public domain W3C validator