![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpancom | Unicode version |
Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
Ref | Expression |
---|---|
mpancom.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
mpancom.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpancom |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpancom.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | id 19 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | mpancom.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2anc 404 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 107 |
This theorem is referenced by: mpan 416 spesbc 2927 onsucelsucr 4340 sucunielr 4342 ordsuc 4394 peano2b 4444 xpiindim 4588 fvelrnb 5367 fliftcnv 5590 riotaprop 5647 unielxp 5960 dmtpos 6037 tpossym 6057 ercnv 6329 cnvct 6582 php5dom 6635 3xpfi 6697 recrecnq 7016 1idpr 7214 eqlei2 7642 lem1 8371 eluzfz1 9508 fzpred 9547 uznfz 9580 fz0fzdiffz0 9604 fzctr 9607 flid 9754 flqeqceilz 9788 faclbnd3 10214 bcn1 10229 isfinite4im 10264 leabs 10570 gcd0id 11311 lcmgcdlem 11400 dvdsnprmd 11448 eltpsg 11801 tg1 11822 cldval 11862 cldss 11868 cldopn 11870 bj-nn0suc0 12149 |
Copyright terms: Public domain | W3C validator |