![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE 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 10 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | mpi.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mpd 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 8 |
This theorem is referenced by: mp2 17 syl6mpi 58 mp2ani 659 mp3an3 1266 3impexpbicom 1367 ee10 1376 merco2 1501 equcomi 1679 ax10 1944 equveli 1988 ax11v2 1992 ax11eq 2193 ax11el 2194 ax11inda 2200 ax11v2-o 2201 pm13.183 2979 sbcth 3060 sbcth2 3129 ssun3 3428 ssun4 3429 uneqdifeq 3638 ralf0 3656 uniintsn 3963 opkth1g 4130 funimass2 5170 fvopab4g 5388 fovcl 5588 ov2ag 5598 ov3 5599 fnfreclem3 6319 |
Copyright terms: Public domain | W3C validator |