![]() |
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: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: syldan 266 ax16i 1735 ceqex 2665 peano2 4261 sotri 4663 relcoi1 4792 f1ocnv 5082 tz6.12c 5146 funbrfv 5155 fnbrfvb 5157 fvmptss2 5190 oprabid 5480 eloprabga 5533 unielxp 5742 f1o2ndf1 5791 tfrlem1 5864 freccl 5932 ecopovtrn 6139 ecopovtrng 6142 ltexnqi 6392 prcdnql 6467 prcunqu 6468 prnmaxl 6471 prnminu 6472 ltprordil 6565 1idprl 6566 1idpru 6567 ltexprlemm 6574 ltexprlemopu 6577 ltexprlemru 6586 recexgt0sr 6701 mulgt0sr 6704 nnind 7711 nnmulcl 7716 nnnegz 8024 ublbneg 8324 ixxssxr 8539 ixxssixx 8541 iccshftri 8633 iccshftli 8635 iccdili 8637 icccntri 8639 1fv 8766 fzo1fzo0n0 8809 elfzonlteqm1 8836 ssfzo12 8850 frec2uzltd 8870 frec2uzrdg 8876 iseqfveq2 8905 cjre 9110 bdfind 9406 bj-nn0sucALT 9438 |
Copyright terms: Public domain | W3C validator |