![]() |
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 986 |
. 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 981 |
This theorem is referenced by: 3adant2l 1233 3adant2r 1234 brelrng 4870 iotam 5220 funimaexglem 5311 fvun2 5596 nnaordi 6522 nnmword 6532 fpmg 6687 prcdnql 7496 prcunqu 7497 prarloc 7515 ltaprg 7631 mul12 8099 add12 8128 addsub 8181 addsubeq4 8185 ppncan 8212 leadd1 8400 ltaddsub2 8407 leaddsub2 8409 lemul1 8563 reapmul1lem 8564 reapadd1 8566 reapcotr 8568 remulext1 8569 div23ap 8661 ltmulgt11 8834 lediv1 8839 lemuldiv 8851 zdiv 9354 iooneg 10001 icoshft 10003 fzaddel 10072 fzshftral 10121 facwordi 10733 abssubge0 11124 climshftlemg 11323 dvdsmul1 11833 divalgb 11943 lcmgcdeq 12096 pcfac 12361 mhmmulg 13055 rmodislmodlem 13534 cnmptcom 14069 hmeof1o2 14079 |
Copyright terms: Public domain | W3C validator |