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

Theorem adantrr 448
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1
Assertion
Ref Expression
adantrr

Proof of Theorem adantrr
StepHypRef Expression
1 simpl 102 . 2
2 adant2.1 . 2
31, 2sylan2 270 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:  ad2ant2r  478  ad2ant2lr  479  dn1dc  866  3ad2antr1  1068  xordidc  1287  po2nr  4037  sotricim  4051  fmptco  5273  fvtp1g  5312  dff13  5350  fcof1o  5372  isocnv  5394  isores2  5396  isoini  5400  f1oiso2  5409  acexmidlemab  5449  ovmpt2df  5574  offval  5661  xp1st  5734  1stconst  5784  cnvf1olem  5787  mpt2xopoveq  5796  nnaordi  6017  nnmordi  6025  erinxp  6116  dom2lem  6188  fundmen  6222  ltsonq  6382  lt2addnq  6388  ltexnqq  6391  prarloclemarch2  6402  enq0sym  6415  genprndl  6504  genprndu  6505  prmuloc  6547  distrlem1prl  6558  distrlem1pru  6559  ltsopr  6570  ltexprlemdisj  6580  ltexprlemfl  6583  ltexprlemfu  6585  addcanprlemu  6589  ltaprg  6592  mulcmpblnrlemg  6668  recexgt0sr  6701  mul4  6942  2addsub  7022  muladd  7177  ltleadd  7236  divmulap3  7438  divcanap7  7479  divadddivap  7485  lemul2a  7606  lemul12b  7608  ltmuldiv2  7622  ltdivmul  7623  ltdivmul2  7625  ledivmul2  7627  lemuldiv2  7629  lt2msq  7633  cju  7694  zextlt  8108  xrlttr  8486  xrre3  8505  ixxdisj  8542  iooshf  8591  icodisj  8630  iccf1o  8642  expsubap  8956  sqrt0rlem  9212
  Copyright terms: Public domain W3C validator