Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpcom | Unicode version |
Description: Modus ponens inference with commutation of antecedents. (Contributed by NM, 17-Mar-1996.) |
Ref | Expression |
---|---|
mpcom.1 | |
mpcom.2 |
Ref | Expression |
---|---|
mpcom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpcom.1 | . 2 | |
2 | mpcom.2 | . . 3 | |
3 | 2 | com12 27 | . 2 |
4 | 1, 3 | mpd 13 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: syldan 266 ax16i 1738 ceqex 2671 peano2 4318 sotri 4720 relcoi1 4849 f1ocnv 5139 tz6.12c 5203 funbrfv 5212 fnbrfvb 5214 fvmptss2 5247 oprabid 5537 eloprabga 5591 unielxp 5800 f1o2ndf1 5849 tfrlem1 5923 freccl 5993 ecopovtrn 6203 ecopovtrng 6206 findcard2d 6348 findcard2sd 6349 ltexnqi 6507 prcdnql 6582 prcunqu 6583 prnmaxl 6586 prnminu 6587 ltprordil 6687 1idprl 6688 1idpru 6689 ltexprlemm 6698 ltexprlemopu 6701 ltexprlemru 6710 recexgt0sr 6858 mulgt0sr 6862 ltrenn 6931 nnindnn 6967 nnind 7930 nnmulcl 7935 nnnegz 8248 ublbneg 8548 ixxssxr 8769 ixxssixx 8771 iccshftri 8863 iccshftli 8865 iccdili 8867 icccntri 8869 1fv 8996 fzo1fzo0n0 9039 elfzonlteqm1 9066 ssfzo12 9080 flqeqceilz 9160 frec2uzltd 9189 frec2uzrdg 9195 iseqfveq2 9228 iseqshft2 9232 monoord 9235 iseqsplit 9238 iseqcaopr3 9240 iseqhomo 9248 cjre 9482 climeu 9817 climub 9864 bdfind 10071 bj-nn0sucALT 10103 |
Copyright terms: Public domain | W3C validator |