Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3com12 | Unicode version |
Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Ref | Expression |
---|---|
3exp.1 |
Ref | Expression |
---|---|
3com12 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ancoma 970 | . 2 | |
2 | 3exp.1 | . 2 | |
3 | 1, 2 | sylbi 120 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: 3adant2l 1214 3adant2r 1215 brelrng 4819 funimaexglem 5255 fvun2 5537 nnaordi 6457 nnmword 6467 fpmg 6621 prcdnql 7406 prcunqu 7407 prarloc 7425 ltaprg 7541 mul12 8008 add12 8037 addsub 8090 addsubeq4 8094 ppncan 8121 leadd1 8309 ltaddsub2 8316 leaddsub2 8318 lemul1 8472 reapmul1lem 8473 reapadd1 8475 reapcotr 8477 remulext1 8478 div23ap 8568 ltmulgt11 8740 lediv1 8745 lemuldiv 8757 zdiv 9257 iooneg 9898 icoshft 9900 fzaddel 9967 fzshftral 10016 facwordi 10625 abssubge0 11013 climshftlemg 11210 dvdsmul1 11720 divalgb 11828 lcmgcdeq 11975 cnmptcom 12768 hmeof1o2 12778 |
Copyright terms: Public domain | W3C validator |