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 619 | . . 3 ⊢ (𝜒 → ¬ ¬ 𝜒) | |
3 | 1, 2 | syl6 33 | . 2 ⊢ (𝜑 → (𝜓 → ¬ ¬ 𝜒)) |
4 | 3 | con2d 614 | 1 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 604 ax-in2 605 |
This theorem is referenced by: con3rr3 623 con3dimp 625 con3 632 nsyld 638 nsyli 639 jcn 641 notbi 656 impidc 844 bijadc 868 pm2.13dc 871 xoranor 1359 mo2n 2034 necon3ad 2369 necon3bd 2370 nelcon3d 2433 ssneld 3130 sscon 3242 difrab 3382 eunex 4522 ndmfvg 5501 nnaord 6458 nnmord 6466 php5 6805 php5dom 6810 supmoti 6939 exmidomniim 7086 mkvprop 7103 enmkvlem 7106 prubl 7408 letr 7962 eqord1 8362 prodge0 8730 lt2msq 8762 nnge1 8861 nzadd 9224 irradd 9561 irrmul 9562 xrletr 9718 frec2uzf1od 10314 zesq 10545 expcanlem 10600 nn0opthd 10607 bccmpl 10639 maxleast 11124 fisumss 11300 dvdsbnd 11855 prm2orodd 12018 coprm 12034 prmndvdsfaclt 12046 hashgcdeq 12129 cos11 13244 bj-nnsn 13380 bj-nnelirr 13599 exmid1stab 13643 ismkvnnlem 13694 nconstwlpolem 13706 |
Copyright terms: Public domain | W3C validator |