![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > mpdi | Structured version Unicode version |
Description: A nested modus ponens deduction. (Contributed by NM, 16-Apr-2005.) (Proof shortened by Mel L. O'Cat, 15-Jan-2008.) |
Ref | Expression |
---|---|
mpdi.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
mpdi.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpdi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpdi.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1i 11 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | mpdi.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mpdd 40 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: mpii 43 pm2.43d 48 impt 157 suctr 4903 tfrlem9 6947 axcc2lem 8709 axdc3lem4 8726 fpwwe2lem8 8908 tskcard 9052 nqereu 9202 mulcmpblnr 9345 lbzbi 11047 fleqceilz 11803 ndvdsadd 13723 gcdneg 13821 ulmcaulem 21985 predpo 27782 wfrlem12 27872 frrlem11 27917 heicant 28567 brabg2 28750 neificl 28790 wlkiswwlk1 30465 frgrawopreglem4 30781 |
Copyright terms: Public domain | W3C validator |