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 1180 | . . 3 |
3 | 2 | com23 78 | . 2 |
4 | 3 | 3imp 1175 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 962 |
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 964 |
This theorem is referenced by: 3coml 1188 syld3an2 1263 3anidm13 1274 eqreu 2876 f1ofveu 5762 acexmid 5773 dfsmo2 6184 f1oeng 6651 ctssdc 6998 ltexprlemdisj 7414 ltexprlemfu 7419 recexprlemss1u 7444 mul32 7892 add32 7921 cnegexlem2 7938 subsub23 7967 subadd23 7974 addsub12 7975 subsub 7992 subsub3 7994 sub32 7996 suble 8202 lesub 8203 ltsub23 8204 ltsub13 8205 ltleadd 8208 div32ap 8452 div13ap 8453 div12ap 8454 divdiv32ap 8480 cju 8719 icc0r 9709 fzen 9823 elfz1b 9870 ioo0 10037 ico0 10039 ioc0 10040 expgt0 10326 expge0 10329 expge1 10330 shftval2 10598 abs3dif 10877 divalgb 11622 ctinf 11943 restin 12345 cnpnei 12388 cnptoprest 12408 psmetsym 12498 xmetsym 12537 |
Copyright terms: Public domain | W3C validator |