![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpid | Unicode version |
Description: A nested modus ponens deduction. (Contributed by NM, 14-Dec-2004.) |
Ref | Expression |
---|---|
mpid.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
mpid.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpid.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1d 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | mpid.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mpdd 41 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: mp2d 47 pm2.43a 51 embantd 56 mpan2d 422 ceqsalt 2667 rspcimdv 2745 fvimacnv 5467 riotass2 5688 pr2ne 6959 0mnnnnn0 8861 caucvgre 10593 climcn1 10916 climcn2 10917 gcdaddm 11467 dvdsgcd 11493 coprmgcdb 11562 nprm 11597 uniopn 11950 metcnp3 12435 cncfco 12491 |
Copyright terms: Public domain | W3C validator |