![]() |
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 1204 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | com23 78 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | 3imp 1195 |
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 982 |
This theorem is referenced by: 3coml 1212 syld3an2 1296 3anidm13 1307 eqreu 2944 f1ofveu 5883 acexmid 5894 dfsmo2 6311 f1oeng 6782 ctssdc 7141 ltexprlemdisj 7634 ltexprlemfu 7639 recexprlemss1u 7664 mul32 8116 add32 8145 cnegexlem2 8162 subsub23 8191 subadd23 8198 addsub12 8199 subsub 8216 subsub3 8218 sub32 8220 suble 8426 lesub 8427 ltsub23 8428 ltsub13 8429 ltleadd 8432 div32ap 8678 div13ap 8679 div12ap 8680 divdiv32ap 8706 cju 8947 icc0r 9955 fzen 10072 elfz1b 10119 ioo0 10289 ico0 10291 ioc0 10292 expgt0 10583 expge0 10586 expge1 10587 shftval2 10866 abs3dif 11145 divalgb 11961 nnwodc 12068 ctinf 12480 grpinvcnv 13009 mulgaddcom 13083 mulgneg2 13093 srgrmhm 13345 ringcom 13382 mulgass2 13407 opprrng 13424 opprring 13426 unitmulcl 13460 islmodd 13606 lmodcom 13646 rmodislmod 13664 restin 14128 cnpnei 14171 cnptoprest 14191 psmetsym 14281 xmetsym 14320 |
Copyright terms: Public domain | W3C validator |