![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > con4i | Structured version Visualization version GIF version |
Description: Inference associated with
con4 112. Its associated inference is mt4 115.
Remark: this can also be proved using notnot 136 followed by nsyl2 142, giving a shorter proof but depending on more axioms (namely, ax-1 6 and ax-2 7). (Contributed by NM, 29-Dec-1992.) |
Ref | Expression |
---|---|
con4i.1 | ⊢ (¬ 𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
con4i | ⊢ (𝜓 → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con4i.1 | . 2 ⊢ (¬ 𝜑 → ¬ 𝜓) | |
2 | con4 112 | . 2 ⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜓 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-3 8 |
This theorem is referenced by: mt4 115 pm2.21i 116 modal-b 2180 sbcbr123 4739 elimasni 5527 ndmfvrcl 6257 brabv 6741 oprssdm 6857 ndmovrcl 6862 omelon2 7119 omopthi 7782 fsuppres 8341 sdomsdomcardi 8835 alephgeom 8943 pwcdadom 9076 rankcf 9637 adderpq 9816 mulerpq 9817 ssnn0fi 12824 sadcp1 15224 setcepi 16785 oduclatb 17191 cntzrcl 17806 pmtrfrn 17924 dprddomcld 18446 dprdsubg 18469 psrbagsn 19543 dsmmbas2 20129 dsmmfi 20130 istps 20786 isusp 22112 dscmet 22424 dscopn 22425 i1f1lem 23501 sqff1o 24953 upgrfi 26031 wwlksnndef 26868 dmadjrnb 28893 axpowprim 31707 opelco3 31802 sltintdifex 31939 nolesgn2ores 31950 nosepdmlem 31958 nosupbnd1lem3 31981 nosupbnd1lem5 31983 nosupbnd2lem1 31986 bj-modal5e 32761 bj-modal4e 32830 bj-snmoore 33193 topdifinffinlem 33325 finxp1o 33359 ax6fromc10 34500 axc711to11 34521 axc5c711to11 34525 pw2f1ocnv 37921 kelac1 37950 relintabex 38204 axc5c4c711toc5 38920 axc5c4c711to11 38923 disjrnmpt2 39689 afvvdm 41542 afvvfunressn 41544 afvvv 41546 afvfv0bi 41553 |
Copyright terms: Public domain | W3C validator |