![]() |
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 411 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: mpan 424 spesbc 3063 onsucelsucr 4528 sucunielr 4530 ordsuc 4583 peano2b 4635 xpiindim 4785 fvelrnb 5587 fliftcnv 5820 riotaprop 5879 unielxp 6203 dmtpos 6285 tpossym 6305 ercnv 6584 cnvct 6839 php5dom 6895 3xpfi 6963 recrecnq 7428 1idpr 7626 eqlei2 8087 lem1 8839 eluzfz1 10067 fzpred 10106 uznfz 10139 fz0fzdiffz0 10166 fzctr 10169 flid 10321 flqeqceilz 10355 faclbnd3 10764 bcn1 10779 isfinite4im 10813 leabs 11124 gcd0id 12021 lcmgcdlem 12120 dvdsnprmd 12168 pcprod 12389 fldivp1 12391 intopsn 12854 mgm1 12857 sgrp1 12897 mnd1 12930 mnd1id 12931 grp1 13073 grp1inv 13074 eqger 13188 eqgid 13190 qusghm 13246 rngressid 13333 ring1 13436 ringressid 13438 subrgsubm 13606 lssex 13695 cncrng 13897 eltpsg 14025 tg1 14044 cldval 14084 cldss 14090 cldopn 14092 psmetdmdm 14309 dvef 14673 relogef 14770 zabsle1 14886 bj-nn0suc0 15188 |
Copyright terms: Public domain | W3C validator |