Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpi | Unicode 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 63 mp2ani 422 pm2.24i 585 simplimdc 790 mp3an3 1257 3impexpbicom 1367 mpisyl 1375 equcomi 1632 equsex 1656 equsexd 1657 spimt 1664 spimeh 1667 equvini 1681 equveli 1682 sbcof2 1731 dveeq2 1736 ax11v2 1741 ax16i 1779 pm13.183 2732 euxfr2dc 2777 sbcth 2828 sbcth2 2901 ssun3 3137 ssun4 3138 ralf0 3344 rext 3970 exss 3982 uniopel 4011 onsucelsucexmid 4273 suc11g 4300 eunex 4304 ordsoexmid 4305 tfisi 4328 finds1 4343 relop 4504 dmrnssfld 4613 iss 4674 relcoi1 4869 nfunv 4953 funimass2 4997 fvssunirng 5210 fvmptg 5269 oprabidlem 5556 fovcl 5626 elovmpt2 5721 tfrlem1 5946 oaword1 6073 diffifi 6378 nlt1pig 6531 dmaddpq 6569 dmmulpq 6570 archnqq 6607 prarloclemarch2 6609 prarloclemlt 6683 cnegex 7286 nnge1 8062 zneo 8448 nn0o1gt2 10305 bdop 10666 bj-nntrans 10746 |
Copyright terms: Public domain | W3C validator |