![]() |
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-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: mp2d 47 pm2.43a 51 embantd 56 mpan2d 428 ceqsalt 2778 rspcimdv 2857 fvimacnv 5652 riotass2 5878 pr2ne 7221 0mnnnnn0 9238 caucvgre 11022 climcn1 11348 climcn2 11349 gcdaddm 12017 dvdsgcd 12045 coprmgcdb 12120 nprm 12155 pcqmul 12335 grpid 12983 uniopn 13961 metcnp3 14471 cncfco 14538 |
Copyright terms: Public domain | W3C validator |