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 1181 | . . 3 |
3 | 2 | com23 78 | . 2 |
4 | 3 | 3imp 1176 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: 3coml 1189 syld3an2 1264 3anidm13 1275 eqreu 2880 f1ofveu 5770 acexmid 5781 dfsmo2 6192 f1oeng 6659 ctssdc 7006 ltexprlemdisj 7438 ltexprlemfu 7443 recexprlemss1u 7468 mul32 7916 add32 7945 cnegexlem2 7962 subsub23 7991 subadd23 7998 addsub12 7999 subsub 8016 subsub3 8018 sub32 8020 suble 8226 lesub 8227 ltsub23 8228 ltsub13 8229 ltleadd 8232 div32ap 8476 div13ap 8477 div12ap 8478 divdiv32ap 8504 cju 8743 icc0r 9739 fzen 9854 elfz1b 9901 ioo0 10068 ico0 10070 ioc0 10071 expgt0 10357 expge0 10360 expge1 10361 shftval2 10630 abs3dif 10909 divalgb 11658 ctinf 11979 restin 12384 cnpnei 12427 cnptoprest 12447 psmetsym 12537 xmetsym 12576 |
Copyright terms: Public domain | W3C validator |