New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > adantrl | Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Ref | Expression |
---|---|
adant2.1 |
Ref | Expression |
---|---|
adantrl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 447 | . 2 | |
2 | adant2.1 | . 2 | |
3 | 1, 2 | sylan2 460 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: ad2ant2l 726 ad2ant2rl 729 consensus 925 3ad2antr2 1121 3ad2antr3 1122 sbcom 2089 tfinltfin 4501 evenodddisj 4516 spfininduct 4540 foco 5279 isocnv 5491 isores2 5493 f1oiso2 5500 fvfullfunlem3 5863 clos1induct 5880 weds 5938 ncspw1eu 6159 tlecg 6230 addccan2nc 6265 nchoicelem12 6300 fnfrec 6320 |
Copyright terms: Public domain | W3C validator |