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

Theorem adantrl 447
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
adantrl

Proof of Theorem adantrl
StepHypRef Expression
1 simpr 103 . 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:  ad2ant2l  477  ad2ant2rl  480  3ad2antr2  1069  3ad2antr3  1070  xordidc  1287  foco  5059  fvun1  5182  isocnv  5394  isores2  5396  f1oiso2  5409  offval  5661  xp2nd  5735  1stconst  5784  2ndconst  5785  tfrlem9  5876  nnmordi  6025  dom2lem  6188  fundmen  6222  ltsonq  6382  ltexnqq  6391  genprndl  6504  genprndu  6505  ltpopr  6569  ltsopr  6570  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemdisj  6580  ltexprlemfl  6583  ltexprlemfu  6585  mulcmpblnrlemg  6668  cnegexlem2  6984  muladd  7177  divadddivap  7485  ltmul12a  7607  lemul12b  7608  cju  7694  zextlt  8108  xrre  8503  ixxdisj  8542  iooshf  8591  icodisj  8630  iccshftr  8632  iccshftl  8634  iccdil  8636  icccntr  8638  iccf1o  8642  fzaddel  8692  fzsubel  8693  expineg2  8918  expsubap  8956  expnbnd  9025
  Copyright terms: Public domain W3C validator