ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad2antrr GIF 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 (𝜑𝜓)
Assertion
Ref Expression
ad2antrr (((𝜑𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem ad2antrr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 261 . 2 ((𝜑𝜃) → 𝜓)
32adantlr 446 1 (((𝜑𝜒) ∧ 𝜃) → 𝜓)
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  6355  dfplpq2  6450  nqpi  6474  nqnq0pi  6534  nq0nn  6538  elinp  6570  elnp1st2nd  6572  genprndl  6617  genprndu  6618  addnqprllem  6623  addnqprulem  6624  addnqprl  6625  addnqpru  6626  addlocpr  6632  nqprloc  6641  prmuloc  6662  mulnqprl  6664  mulnqpru  6665  mullocpr  6667  distrlem1prl  6678  distrlem1pru  6679  ltsopr  6692  ltexprlemopl  6697  ltexprlemopu  6699  ltexprlemloc  6703  ltexprlemrl  6706  ltexprlemru  6708  addcanprleml  6710  addcanprlemu  6711  recexprlemloc  6727  recexprlem1ssl  6729  recexprlem1ssu  6730  aptiprleml  6735  aptiprlemu  6736  archpr  6739  cauappcvgprlemm  6741  cauappcvgprlemopl  6742  cauappcvgprlemlol  6743  cauappcvgprlemladdfu  6750  cauappcvgprlemladdfl  6751  cauappcvgprlemladdru  6752  archrecpr  6760  caucvgprlemnkj  6762  caucvgprlemm  6764  caucvgprlemopl  6765  caucvgprlemlol  6766  caucvgprlemdisj  6770  caucvgprlemloc  6771  caucvgprlemladdfu  6773  caucvgprprlemnkltj  6785  caucvgprprlemnkeqj  6786  caucvgprprlemnjltk  6787  caucvgprprlemml  6790  caucvgprprlemopl  6793  caucvgprprlemlol  6794  caucvgprprlemdisj  6798  caucvgprprlemexbt  6802  caucvgprprlemexb  6803  caucvgprprlemaddq  6804  mulgt0sr  6860  caucvgsrlemcau  6875  caucvgsrlemoffcau  6880  caucvgsrlemoffres  6882  axcaucvglemcau  6970  axcaucvglemres  6971  cnegexlem1  7184  cnegex  7187  apsym  7595  apcotr  7596  apadd1  7597  mulext1  7601  mulge0  7608  apti  7611  conjmulap  7703  lemulge11  7830  creui  7910  nndiv  7952  zaddcllemneg  8282  eluzuzle  8479  divfnzn  8554  qapne  8572  xrltso  8715  xrre  8731  xrre3  8733  ixxss12  8773  elioc2  8803  elico2  8804  elicc2  8805  fzm1  8960  fzneuz  8961  eluzgtdifelfzo  9051  elfzonelfzo  9084  qtri3or  9096  qbtwnzlemstep  9101  qbtwnzlemex  9103  qbtwnz  9104  frecuzrdgrrn  9168  iseqid3s  9220  expival  9231  expap0  9259  ovshftex  9394  2shfti  9406  cjap  9480  caucvgrelemcau  9553  cvg1nlemcau  9557  cvg1nlemres  9558  recvguniq  9567  resqrexlemdecn  9584  resqrexlemcalc3  9588  resqrexlemcvg  9591  resqrexlemoverl  9593  leabs  9646  absexpzap  9650  ltabs  9657  abslt  9658  absle  9659  2clim  9796  climshftlemg  9797  climsqz  9829  climsqz2  9830  climrecvg1n  9841  climcvg1nlem  9842  serif0  9845  sqrt2irr  9852  bj-findis  10078  qdencn  10097
  Copyright terms: Public domain W3C validator