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: wi 4 |
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 424 ceqsalt 2712 rspcimdv 2790 fvimacnv 5535 riotass2 5756 pr2ne 7048 0mnnnnn0 9009 caucvgre 10753 climcn1 11077 climcn2 11078 gcdaddm 11672 dvdsgcd 11700 coprmgcdb 11769 nprm 11804 uniopn 12168 metcnp3 12680 cncfco 12747 |
Copyright terms: Public domain | W3C validator |