New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > adantrd | Unicode version |
Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.) |
Ref | Expression |
---|---|
adantrd.1 |
Ref | Expression |
---|---|
adantrd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 443 | . 2 | |
2 | adantrd.1 | . 2 | |
3 | 1, 2 | syl5 28 | 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: syldan 456 jaoa 496 prlem1 928 cad0 1400 equveli 1988 2eu3 2286 unineq 3505 tfinltfinlem1 4500 sfintfin 4532 vfinncvntnn 4548 fvun1 5379 fnasrn 5417 fconst5 5455 fconstfv 5456 enadjlem1 6059 leltctr 6212 addcdi 6250 nmembers1lem3 6270 nchoicelem12 6300 |
Copyright terms: Public domain | W3C validator |