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  6441  prarloclem3step  6478  genpml  6499  genpmu  6500  addnqprl  6511  addnqpru  6512  appdivnq  6543  mulnqprl  6548  mulnqpru  6549  mullocpr  6551  ltexprlemfl  6582  ltexprlemfu  6584  ltmprr  6613  archpr  6614  cauappcvgprlemm  6616  recexgt0sr  6681  mulgt0sr  6684  cnegex  6966  apirr  7369  mulge0  7383  lemul12a  7589  lediv2a  7622  creur  7672  nndiv  7715  zaddcllemneg  8040  peano5uzti  8102  divfnzn  8312  xrltso  8467  elioc2  8555  elico2  8556  elicc2  8557
  Copyright terms: Public domain W3C validator