![]() |
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 985 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3exp.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylbi 121 |
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-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: 3adant2l 1232 3adant2r 1233 brelrng 4860 iotam 5210 funimaexglem 5301 fvun2 5585 nnaordi 6511 nnmword 6521 fpmg 6676 prcdnql 7485 prcunqu 7486 prarloc 7504 ltaprg 7620 mul12 8088 add12 8117 addsub 8170 addsubeq4 8174 ppncan 8201 leadd1 8389 ltaddsub2 8396 leaddsub2 8398 lemul1 8552 reapmul1lem 8553 reapadd1 8555 reapcotr 8557 remulext1 8558 div23ap 8650 ltmulgt11 8823 lediv1 8828 lemuldiv 8840 zdiv 9343 iooneg 9990 icoshft 9992 fzaddel 10061 fzshftral 10110 facwordi 10722 abssubge0 11113 climshftlemg 11312 dvdsmul1 11822 divalgb 11932 lcmgcdeq 12085 pcfac 12350 mhmmulg 13029 rmodislmodlem 13445 cnmptcom 13837 hmeof1o2 13847 |
Copyright terms: Public domain | W3C validator |