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 624 | . . 3 ⊢ (𝜒 → ¬ ¬ 𝜒) | |
3 | 1, 2 | syl6 33 | . 2 ⊢ (𝜑 → (𝜓 → ¬ ¬ 𝜒)) |
4 | 3 | con2d 619 | 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 609 ax-in2 610 |
This theorem is referenced by: con3rr3 628 con3dimp 630 con3 637 nsyld 643 nsyli 644 jcn 646 notbi 661 impidc 853 bijadc 877 pm2.13dc 880 xoranor 1372 mo2n 2047 necon3ad 2382 necon3bd 2383 nelcon3d 2446 ssneld 3149 sscon 3261 difrab 3401 eunex 4545 ndmfvg 5527 nnaord 6488 nnmord 6496 php5 6836 php5dom 6841 supmoti 6970 exmidomniim 7117 mkvprop 7134 enmkvlem 7137 prubl 7448 letr 8002 eqord1 8402 prodge0 8770 lt2msq 8802 nnge1 8901 nzadd 9264 irradd 9605 irrmul 9606 xrletr 9765 frec2uzf1od 10362 zesq 10594 expcanlem 10649 nn0opthd 10656 bccmpl 10688 maxleast 11177 fisumss 11355 dvdsbnd 11911 prm2orodd 12080 coprm 12098 prmndvdsfaclt 12110 hashgcdeq 12193 cos11 13568 bj-nnsn 13768 bj-nnelirr 13988 exmid1stab 14033 ismkvnnlem 14084 nconstwlpolem 14096 |
Copyright terms: Public domain | W3C validator |