Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3com23 | Unicode version |
Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.) |
Ref | Expression |
---|---|
3exp.1 |
Ref | Expression |
---|---|
3com23 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . . 4 | |
2 | 1 | 3exp 1103 | . . 3 |
3 | 2 | com23 72 | . 2 |
4 | 3 | 3imp 1098 | 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: 3coml 1111 syld3an2 1182 3anidm13 1193 eqreu 2733 f1ofveu 5500 acexmid 5511 dfsmo2 5902 f1oeng 6237 ltexprlemdisj 6704 ltexprlemfu 6709 recexprlemss1u 6734 mul32 7143 add32 7170 cnegexlem2 7187 subsub23 7216 subadd23 7223 addsub12 7224 subsub 7241 subsub3 7243 sub32 7245 suble 7435 lesub 7436 ltsub23 7437 ltsub13 7438 ltleadd 7441 div32ap 7671 div13ap 7672 div12ap 7673 divdiv32ap 7696 cju 7913 icc0r 8795 fzen 8907 elfz1b 8952 elfzmlbmOLD 8989 expival 9257 expgt0 9288 expge0 9291 expge1 9292 shftval2 9427 abs3dif 9701 |
Copyright terms: Public domain | W3C validator |