![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3com23 | Structured version Visualization version 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 1207 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | com23 81 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | 3imp 1202 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 189 df-an 373 df-3an 987 |
This theorem is referenced by: 3coml 1215 syld3an2 1315 3anidm13 1326 eqreu 3230 f1ofveu 6285 curry2f 6892 dfsmo2 7066 nneob 7353 f1oeng 7588 suppr 7987 infdif 8639 axdclem2 8950 gchen1 9050 grumap 9233 grudomon 9242 mul32 9800 add32 9847 subsub23 9880 subadd23 9887 addsub12 9888 subsub 9904 subsub3 9906 sub32 9908 suble 10092 lesub 10093 ltsub23 10094 ltsub13 10095 ltleadd 10097 div32 10290 div13 10291 div12 10292 divdiv32 10315 cju 10605 infssuzle 11244 infmssuzleOLD 11246 ioo0 11661 ico0 11682 ioc0 11683 icc0 11684 fzen 11816 elfz1b 11864 elfzmlbmOLD 11901 modcyc 12132 expgt0 12305 expge0 12308 expge1 12309 2cshwcom 12915 shftval2 13138 abs3dif 13394 divalgb 14385 submrc 15534 mrieqv2d 15545 pltnlt 16214 pltn2lp 16215 tosso 16282 latnle 16331 latabs1 16333 lubel 16368 ipopos 16406 grpinvcnv 16722 mulgneg2 16785 oppgmnd 17005 oddvdsnn0 17193 oddvds 17196 odmulg 17207 odcl2 17216 lsmcomx 17494 srgrmhm 17769 ringcom 17809 mulgass2 17829 opprring 17859 irredrmul 17935 irredlmul 17936 isdrngrd 18001 islmodd 18097 lmodcom 18134 opprdomn 18525 zntoslem 19127 ipcl 19200 maducoevalmin1 19677 rintopn 19939 opnnei 20136 restin 20182 cnpnei 20280 cnprest 20305 ordthaus 20400 kgen2ss 20570 hausflim 20996 fclsfnflim 21042 cnpfcf 21056 opnsubg 21122 cuspcvg 21316 psmetsym 21326 xmetsym 21362 ngpdsr 21618 ngpds2r 21620 ngpds3r 21622 clmmulg 22124 iscau2 22247 dgr1term 23214 cxpeq0 23623 cxpge0 23628 relogbzcl 23711 grpoidinvlem2 25933 grpoinvdiv 25973 gxcl 25993 nvpncan 26278 nvsub 26296 nvabs 26302 nvelbl 26325 ipval2lem2 26340 ipval2lem5 26346 dipcj 26353 diporthcom 26355 dipdi 26484 dipassr 26487 dipsubdi 26490 hlipcj 26563 hvadd32 26687 hvsub32 26698 his5 26739 hoadd32 27436 hosubsub 27470 unopf1o 27569 adj2 27587 adjvalval 27590 adjlnop 27739 leopmul2i 27788 cvntr 27945 mdsymlem5 28060 sumdmdii 28068 supxrnemnf 28354 odutos 28424 tlt2 28425 tosglblem 28430 archiabl 28515 unitdivcld 28707 bnj605 29718 bnj607 29727 ghomf1olem 30312 gcd32 30387 cgrrflx 30754 cgrcom 30757 cgrcomr 30764 btwntriv1 30783 cgr3com 30820 colineartriv2 30835 segleantisym 30882 seglelin 30883 btwnoutside 30892 clsint2 30985 dissneqlem 31742 ftc1anclem5 32021 heibor1 32142 rngoidl 32257 ispridlc 32303 opltcon3b 32770 cmtcomlemN 32814 cmtcomN 32815 cmt3N 32817 cmtbr3N 32820 cvrval2 32840 cvrnbtwn4 32845 leatb 32858 atlrelat1 32887 hlatlej2 32941 hlateq 32964 hlrelat5N 32966 snatpsubN 33315 pmap11 33327 paddcom 33378 sspadd2 33381 paddss12 33384 cdleme51finvN 34123 cdleme51finvtrN 34125 cdlemeiota 34152 cdlemg2jlemOLDN 34160 cdlemg2klem 34162 cdlemg4b1 34176 cdlemg4b2 34177 trljco2 34308 tgrpabl 34318 tendoplcom 34349 cdleml6 34548 erngdvlem3-rN 34565 dia11N 34616 dib11N 34728 dih11 34833 nerabdioph 35652 monotoddzzfi 35790 fzneg 35832 jm2.19lem2 35845 nzss 36666 sineq0ALT 37334 lincvalsng 40262 reccot 40531 |
Copyright terms: Public domain | W3C validator |