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 892 | . 2 | |
2 | 3exp.1 | . 2 | |
3 | 1, 2 | sylbi 114 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 885 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: 3adant2l 1129 3adant2r 1130 brelrng 4565 funimaexglem 4982 fvun2 5240 nnaordi 6081 nnmword 6091 prcdnql 6582 prcunqu 6583 prarloc 6601 ltaprg 6717 mul12 7142 add12 7169 addsub 7222 addsubeq4 7226 ppncan 7253 leadd1 7425 ltaddsub2 7432 leaddsub2 7434 lemul1 7584 reapmul1lem 7585 reapadd1 7587 reapcotr 7589 remulext1 7590 div23ap 7670 ltmulgt11 7830 lediv1 7835 lemuldiv 7847 zdiv 8328 iooneg 8856 icoshft 8858 fzaddel 8922 fzshftral 8970 abssubge0 9698 climshftlemg 9823 |
Copyright terms: Public domain | W3C validator |