NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  adantld Unicode version

Theorem adantld 453
Description: Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)
Hypothesis
Ref Expression
adantld.1
Assertion
Ref Expression
adantld

Proof of Theorem adantld
StepHypRef Expression
1 simpr 447 . 2
2 adantld.1 . 2
31, 2syl5 28 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wa 358
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
This theorem is referenced by:  jaoa  496  dedlema  920  dedlemb  921  prlem1  928  spimed  1977  equveli  1988  2eu3  2286  unineq  3505  tfinpw1  4494  tfinltfinlem1  4500  sfinltfin  4535  spfinsfincl  4539  vfinspsslem1  4550  clos1conn  5879  taddc  6229  nchoicelem12  6300
  Copyright terms: Public domain W3C validator