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 111. Its associated inference is mt4 114. (Contributed by NM, 29-Dec-1992.) |
Ref | Expression |
---|---|
con4i.1 | ⊢ (¬ 𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
con4i | ⊢ (𝜓 → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con4i.1 | . 2 ⊢ (¬ 𝜑 → ¬ 𝜓) | |
2 | con4 111 | . 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 114 pm2.21i 115 modal-b 2127 sbcbr123 4636 elimasni 5411 ndmfvrcl 6129 brabv 6597 oprssdm 6713 ndmovrcl 6718 omelon2 6969 omopthi 7624 fsuppres 8183 sdomsdomcardi 8680 alephgeom 8788 pwcdadom 8921 rankcf 9478 adderpq 9657 mulerpq 9658 ssnn0fi 12646 sadcp1 15015 setcepi 16561 oduclatb 16967 cntzrcl 17583 pmtrfrn 17701 dprddomcld 18223 dprdsubg 18246 psrbagsn 19316 dsmmbas2 19900 dsmmfi 19901 istps 20551 isusp 21875 dscmet 22187 dscopn 22188 i1f1lem 23262 sqff1o 24708 upgrfi 25758 umgrafi 25851 usgraedgrnv 25906 nbgranself2 25965 wwlknndef 26265 clwwlknndef 26301 dmadjrnb 28149 axpowprim 30835 opelco3 30923 sltintdifex 31060 bj-modal5e 31825 bj-modal4e 31892 topdifinffinlem 32371 finxp1o 32405 ax6fromc10 33199 axc711to11 33220 axc5c711to11 33224 pw2f1ocnv 36622 kelac1 36651 relintabex 36906 axc5c4c711toc5 37625 axc5c4c711to11 37628 disjrnmpt2 38370 afvvdm 39870 afvvfunressn 39872 afvvv 39874 afvfv0bi 39881 wwlksnndef 41111 clwwlksnndef 41198 |
Copyright terms: Public domain | W3C validator |