![]() |
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 432 pm2.24i 623 simplimdc 860 mp3an3 1326 3impexpbicom 1438 mpisyl 1446 equcomi 1704 equsex 1728 equsexd 1729 spimt 1736 spimeh 1739 equvini 1758 equveli 1759 sbcof2 1810 dveeq2 1815 ax11v2 1820 ax16i 1858 pm13.183 2877 euxfr2dc 2924 sbcth 2978 sbcth2 3052 ssun3 3302 ssun4 3303 ralf0 3528 exmidexmid 4198 rext 4217 exss 4229 uniopel 4258 onsucelsucexmid 4531 suc11g 4558 eunex 4562 ordsoexmid 4563 tfisi 4588 finds1 4603 omsinds 4623 relop 4779 dmrnssfld 4892 iss 4955 relcoi1 5162 nfunv 5251 funimass2 5296 fvssunirng 5532 fvmptg 5594 oprabidlem 5908 fovcl 5982 elovmpo 6074 tfrlem1 6311 oaword1 6474 0domg 6839 diffifi 6896 exmidpw 6910 djulclb 7056 0ct 7108 nlt1pig 7342 dmaddpq 7380 dmmulpq 7381 archnqq 7418 prarloclemarch2 7420 prarloclemlt 7494 cnegex 8137 nnge1 8944 zneo 9356 fsum2d 11445 fsumabs 11475 fsumiun 11487 fprod2d 11633 efne0 11688 nn0o1gt2 11912 ennnfonelemex 12417 qtopbasss 14106 reeff1o 14279 coseq0negpitopi 14342 cos02pilt1 14357 logltb 14380 bdop 14712 bj-nntrans 14788 |
Copyright terms: Public domain | W3C validator |