![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > con3d | GIF version |
Description: A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
con3d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
con3d | ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con3d.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | notnot 592 | . . 3 ⊢ (𝜒 → ¬ ¬ 𝜒) | |
3 | 1, 2 | syl6 33 | . 2 ⊢ (𝜑 → (𝜓 → ¬ ¬ 𝜒)) |
4 | 3 | con2d 587 | 1 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in1 577 ax-in2 578 |
This theorem is referenced by: con3rr3 596 con3dimp 597 con3 604 nsyld 610 nsyli 611 mth8 612 notbid 625 impidc 789 bijadc 810 pm2.13dc 813 xoranor 1309 mo2n 1970 necon3ad 2288 necon3bd 2289 ssneld 3002 sscon 3107 difrab 3239 eunex 4306 ndmfvg 5230 nnaord 6141 nnmord 6149 php5 6383 php5dom 6388 supmoti 6455 prubl 6727 letr 7250 prodge0 7988 lt2msq 8020 nnge1 8118 nzadd 8473 irradd 8801 irrmul 8802 xrletr 8943 frec2uzf1od 9477 zesq 9677 expcanlem 9729 nn0opthd 9735 bccmpl 9767 maxleast 10226 dvdsbnd 10481 prm2orodd 10641 coprm 10656 prmndvdsfaclt 10668 bj-notbi 10859 bj-nnelirr 10891 |
Copyright terms: Public domain | W3C validator |