Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpi | GIF version |
Description: A nested modus ponens inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.) |
Ref | Expression |
---|---|
mpi.1 | ⊢ 𝜓 |
mpi.2 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
mpi | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpi.1 | . . 3 ⊢ 𝜓 | |
2 | 1 | a1i 9 | . 2 ⊢ (𝜑 → 𝜓) |
3 | mpi.2 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 2, 3 | mpd 13 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: mp2 16 syl6mpi 64 mp2ani 428 pm2.24i 597 simplimdc 830 mp3an3 1289 3impexpbicom 1399 mpisyl 1407 equcomi 1665 equsex 1691 equsexd 1692 spimt 1699 spimeh 1702 equvini 1716 equveli 1717 sbcof2 1766 dveeq2 1771 ax11v2 1776 ax16i 1814 pm13.183 2796 euxfr2dc 2842 sbcth 2895 sbcth2 2968 ssun3 3211 ssun4 3212 ralf0 3436 exmidexmid 4090 rext 4107 exss 4119 uniopel 4148 onsucelsucexmid 4415 suc11g 4442 eunex 4446 ordsoexmid 4447 tfisi 4471 finds1 4486 omsinds 4505 relop 4659 dmrnssfld 4772 iss 4835 relcoi1 5040 nfunv 5126 funimass2 5171 fvssunirng 5404 fvmptg 5465 oprabidlem 5770 fovcl 5844 elovmpo 5939 tfrlem1 6173 oaword1 6335 0domg 6699 diffifi 6756 exmidpw 6770 djulclb 6908 0ct 6960 nlt1pig 7117 dmaddpq 7155 dmmulpq 7156 archnqq 7193 prarloclemarch2 7195 prarloclemlt 7269 cnegex 7908 nnge1 8711 zneo 9120 fsum2d 11172 fsumabs 11202 fsumiun 11214 efne0 11311 nn0o1gt2 11529 ennnfonelemex 11854 qtopbasss 12617 coseq0negpitopi 12844 cos02pilt1 12859 bdop 13000 bj-nntrans 13076 |
Copyright terms: Public domain | W3C validator |