![]() |
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-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: mp2 16 syl6mpi 64 mp2ani 424 pm2.24i 589 simplimdc 796 mp3an3 1263 3impexpbicom 1373 mpisyl 1381 equcomi 1638 equsex 1664 equsexd 1665 spimt 1672 spimeh 1675 equvini 1689 equveli 1690 sbcof2 1739 dveeq2 1744 ax11v2 1749 ax16i 1787 pm13.183 2755 euxfr2dc 2801 sbcth 2854 sbcth2 2927 ssun3 3166 ssun4 3167 ralf0 3389 exmidexmid 4037 rext 4051 exss 4063 uniopel 4092 onsucelsucexmid 4359 suc11g 4386 eunex 4390 ordsoexmid 4391 tfisi 4415 finds1 4430 omsinds 4448 relop 4599 dmrnssfld 4709 iss 4771 relcoi1 4975 nfunv 5060 funimass2 5105 fvssunirng 5333 fvmptg 5393 oprabidlem 5694 fovcl 5764 elovmpt2 5859 tfrlem1 6087 oaword1 6246 0domg 6607 diffifi 6664 exmidpw 6678 djulclb 6801 nlt1pig 6954 dmaddpq 6992 dmmulpq 6993 archnqq 7030 prarloclemarch2 7032 prarloclemlt 7106 cnegex 7714 nnge1 8499 zneo 8901 fsum2d 10883 fsumabs 10913 fsumiun 10925 efne0 11022 nn0o1gt2 11237 bdop 12032 bj-nntrans 12112 |
Copyright terms: Public domain | W3C validator |