ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad2antrr Structured version   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  2598  reupick  3215  euotd  3982  ralxfrd  4160  foun  5088  f1oprg  5111  dffo4  5258  foeqcnvco  5373  fliftfun  5379  isotr  5399  riotass2  5437  ovmpt2dxf  5568  mpt2xopoveq  5796  tfrlem1  5864  tfrlemibacc  5881  tfrlemibfn  5883  tfrlemi14d  5888  tfrexlem  5889  nnmordi  6025  eroprf  6135  f1imaen2g  6209  dfplpq2  6338  nqpi  6362  nqnq0pi  6420  nq0nn  6424  elinp  6456  elnp1st2nd  6458  genprndl  6503  genprndu  6504  addnqprllem  6509  addnqprulem  6510  addnqprl  6511  addnqpru  6512  addlocpr  6518  nqprloc  6527  prmuloc  6546  mulnqprl  6548  mulnqpru  6549  mullocpr  6551  distrlem1prl  6557  distrlem1pru  6558  ltsopr  6569  ltexprlemopl  6574  ltexprlemopu  6576  ltexprlemloc  6580  ltexprlemrl  6583  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  recexprlemloc  6602  recexprlem1ssl  6604  recexprlem1ssu  6605  aptiprleml  6610  aptiprlemu  6611  archpr  6614  cauappcvgprlemm  6616  cauappcvgprlemopl  6617  cauappcvgprlemlol  6618  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  mulgt0sr  6684  cnegexlem1  6963  cnegex  6966  apsym  7370  apcotr  7371  apadd1  7372  mulext1  7376  mulge0  7383  apti  7386  conjmulap  7467  lemulge11  7593  creui  7673  nndiv  7715  zaddcllemneg  8040  eluzuzle  8237  divfnzn  8312  qapne  8330  xrltso  8467  xrre  8483  xrre3  8485  ixxss12  8525  elioc2  8555  elico2  8556  elicc2  8557  fzm1  8712  fzneuz  8713  eluzgtdifelfzo  8803  elfzonelfzo  8836  frecuzrdgrrn  8855  expival  8891  expap0  8919  cjap  9114  bj-findis  9409
  Copyright terms: Public domain W3C validator