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  5057  fvun1  5180  isocnv  5392  isores2  5394  f1oiso2  5407  offval  5658  xp2nd  5732  1stconst  5781  2ndconst  5782  tfrlem9  5873  nnmordi  6018  dom2lem  6181  fundmen  6215  ltsonq  6375  ltexnqq  6384  genprndl  6497  genprndu  6498  ltpopr  6559  ltsopr  6560  ltexprlemm  6564  ltexprlemopl  6565  ltexprlemopu  6567  ltexprlemdisj  6570  ltexprlemfl  6573  ltexprlemfu  6575  mulcmpblnrlemg  6620  cnegexlem2  6936  muladd  7129  divadddivap  7437  ltmul12a  7558  lemul12b  7559  cju  7645  zextlt  8057  xrre  8451  ixxdisj  8490  iooshf  8539  icodisj  8578  iccshftr  8580  iccshftl  8582  iccdil  8584  icccntr  8586  iccf1o  8590  fzaddel  8638  fzsubel  8639
  Copyright terms: Public domain W3C validator