![]() |
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: ![]() |
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 624 simplimdc 861 mp3an3 1337 3impexpbicom 1449 mpisyl 1457 equcomi 1715 equsex 1739 equsexd 1740 spimt 1747 spimeh 1750 equvini 1769 equveli 1770 sbcof2 1821 dveeq2 1826 ax11v2 1831 ax16i 1869 pm13.183 2890 euxfr2dc 2937 sbcth 2991 sbcth2 3065 ssun3 3315 ssun4 3316 ralf0 3541 exmidexmid 4214 rext 4233 exss 4245 uniopel 4274 onsucelsucexmid 4547 suc11g 4574 eunex 4578 ordsoexmid 4579 tfisi 4604 finds1 4619 omsinds 4639 relop 4795 dmrnssfld 4908 iss 4971 relcoi1 5178 nfunv 5268 funimass2 5313 fvssunirng 5549 fvmptg 5613 oprabidlem 5928 elovmpo 6096 tfrlem1 6334 oaword1 6497 0domg 6866 diffifi 6923 exmidpw 6937 djulclb 7085 0ct 7137 nlt1pig 7371 dmaddpq 7409 dmmulpq 7410 archnqq 7447 prarloclemarch2 7449 prarloclemlt 7523 cnegex 8166 nnge1 8973 zneo 9385 fsum2d 11478 fsumabs 11508 fsumiun 11520 fprod2d 11666 efne0 11721 nn0o1gt2 11945 ennnfonelemex 12468 qtopbasss 14498 reeff1o 14671 coseq0negpitopi 14734 cos02pilt1 14749 logltb 14772 bdop 15105 bj-nntrans 15181 |
Copyright terms: Public domain | W3C validator |