New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > con1d | Unicode version |
Description: A contraposition deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
con1d.1 |
Ref | Expression |
---|---|
con1d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con1d.1 | . . 3 | |
2 | notnot1 114 | . . 3 | |
3 | 1, 2 | syl6 29 | . 2 |
4 | 3 | con4d 97 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem is referenced by: mt3d 117 con1 120 con3d 125 pm2.24d 135 pm2.61d 150 pm2.8 823 dedlem0b 919 meredith 1404 19.9ht 1778 19.9tOLD 1857 ax12olem3 1929 necon3bd 2553 necon4bd 2578 necon1ad 2583 sspss 3368 neldif 3391 nnsucelr 4428 funiunfv 5467 |
Copyright terms: Public domain | W3C validator |