![]() |
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 2894 euxfr2dc 2941 sbcth 2995 sbcth2 3069 ssun3 3320 ssun4 3321 ralf0 3545 exmidexmid 4221 rext 4240 exss 4252 uniopel 4281 onsucelsucexmid 4554 suc11g 4581 eunex 4585 ordsoexmid 4586 tfisi 4611 finds1 4626 omsinds 4646 relop 4802 dmrnssfld 4915 iss 4978 relcoi1 5185 nfunv 5275 funimass2 5320 fvssunirng 5557 fvmptg 5621 oprabidlem 5937 elovmpo 6105 tfrlem1 6348 oaword1 6511 0domg 6880 diffifi 6937 exmidpw 6951 djulclb 7100 0ct 7152 nlt1pig 7387 dmaddpq 7425 dmmulpq 7426 archnqq 7463 prarloclemarch2 7465 prarloclemlt 7539 cnegex 8183 nnge1 8991 zneo 9404 fsum2d 11552 fsumabs 11582 fsumiun 11594 fprod2d 11740 efne0 11795 nn0o1gt2 12020 ennnfonelemex 12545 qtopbasss 14646 ivthdichlem 14762 reeff1o 14836 coseq0negpitopi 14899 cos02pilt1 14914 logltb 14937 gausslemma2dlem0i 15101 bdop 15291 bj-nntrans 15367 |
Copyright terms: Public domain | W3C validator |