ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad2antlr Structured version   GIF version

Theorem ad2antlr 458
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
ad2antlr (((χ φ) θ) → ψ)

Proof of Theorem ad2antlr
StepHypRef Expression
1 ad2ant.1 . . 3 (φψ)
21adantr 261 . 2 ((φ θ) → ψ)
32adantll 445 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:  ad3antlr  462  simplr  482  simplrl  487  simplrr  488  en2lp  4232  xpid11m  4500  foun  5088  f1oprg  5111  fcof1o  5372  foeqcnvco  5373  f1eqcocnv  5374  caovord3  5616  f1o2ndf1  5791  smores2  5850  frecrdg  5931  nnaordex  6036  xpdom2  6241  dfplpq2  6338  recclnq  6376  subhalfnqq  6397  distrnq0  6442  prarloclem3step  6479  genpml  6500  genpmu  6501  addnqprl  6512  addnqpru  6513  appdivnq  6544  mulnqprl  6549  mulnqpru  6550  mullocpr  6552  ltexprlemfl  6583  ltexprlemfu  6585  ltmprr  6614  archpr  6615  cauappcvgprlemm  6617  caucvgprlemladdrl  6649  recexgt0sr  6701  mulgt0sr  6704  cnegex  6986  apirr  7389  mulge0  7403  lemul12a  7609  lediv2a  7642  creur  7692  nndiv  7735  zaddcllemneg  8060  peano5uzti  8122  divfnzn  8332  xrltso  8487  elioc2  8575  elico2  8576  elicc2  8577
  Copyright terms: Public domain W3C validator