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 58 mp2ani 408 pm2.24i 553 simplimdc 757 mp3an3 1221 3impexpbicom 1327 mpisyl 1335 equcomi 1592 equsex 1616 equsexd 1617 spimt 1624 spimeh 1627 equvini 1641 equveli 1642 sbcof2 1691 dveeq2 1696 ax11v2 1701 ax16i 1738 pm13.183 2681 euxfr2dc 2726 sbcth 2777 sbcth2 2845 ssun3 3108 ssun4 3109 ralf0 3324 rext 3951 exss 3963 uniopel 3993 onsucelsucexmid 4255 suc11g 4281 eunex 4285 ordsoexmid 4286 tfisi 4310 finds1 4325 relop 4486 dmrnssfld 4595 iss 4654 relcoi1 4849 nfunv 4933 funimass2 4977 fvssunirng 5190 fvmptg 5248 oprabidlem 5536 fovcl 5606 elovmpt2 5701 tfrlem1 5923 oaword1 6050 diffifi 6351 nlt1pig 6439 dmaddpq 6477 dmmulpq 6478 archnqq 6515 prarloclemarch2 6517 prarloclemlt 6591 cnegex 7189 nnge1 7937 zneo 8339 bdop 9995 bj-nntrans 10076 |
Copyright terms: Public domain | W3C validator |