New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3adant2 | Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
Ref | Expression |
---|---|
3adant.1 |
Ref | Expression |
---|---|
3adant2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpb 953 | . 2 | |
2 | 3adant.1 | . 2 | |
3 | 1, 2 | syl 15 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 w3a 934 |
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 df-3an 936 |
This theorem is referenced by: 3ad2ant1 976 eupickb 2269 vtoclegft 2926 eqeu 3007 leltfintr 4458 ltfintr 4459 ltfintri 4466 ncfineleq 4477 tfinltfin 4501 vfinspnn 4541 vfintle 4546 phi11lem1 4595 fnco 5191 dff1o2 5291 fnimapr 5374 f1elima 5474 f1ocnvfvb 5479 fununiq 5517 oprssov 5603 ncspw1eu 6159 leaddc1 6214 letc 6231 addcdir 6251 lemuc1 6253 lecadd2 6266 nchoicelem17 6305 |
Copyright terms: Public domain | W3C validator |