![]() |
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 952 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3exp.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylbi 120 |
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-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 947 |
This theorem is referenced by: 3adant2l 1193 3adant2r 1194 brelrng 4730 funimaexglem 5164 fvun2 5442 nnaordi 6358 nnmword 6368 fpmg 6522 prcdnql 7240 prcunqu 7241 prarloc 7259 ltaprg 7375 mul12 7814 add12 7843 addsub 7896 addsubeq4 7900 ppncan 7927 leadd1 8111 ltaddsub2 8118 leaddsub2 8120 lemul1 8273 reapmul1lem 8274 reapadd1 8276 reapcotr 8278 remulext1 8279 div23ap 8364 ltmulgt11 8532 lediv1 8537 lemuldiv 8549 zdiv 9043 iooneg 9664 icoshft 9666 fzaddel 9732 fzshftral 9781 facwordi 10379 abssubge0 10766 climshftlemg 10963 dvdsmul1 11363 divalgb 11470 lcmgcdeq 11610 cnmptcom 12309 |
Copyright terms: Public domain | W3C validator |