com23 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem com23 32

Description: Commutation of antecedents. Swap 2nd and 3rd.

**Hypothesis**
Ref	Expression
com3.1

**Assertion**
Ref	Expression
com23

**Proof of Theorem com23**
Step	Hyp	Ref	Expression
1		com3.1	. 2
2		pm2.04 30	. 2
3	1, 2	syl 10	1

Colors of variables: wff set class

Syntax hints:

wi 3

This theorem is referenced by: com13 33 com3l 34 com24 37 mpii 45 pm2.86 69 impt 141 ancom2s 486 prth 554 elimant 682 pclem6 739 dedlem0b 759 dedlemb 761 3com23 837 meredith 921 a4imt 1154 cbv1 1158 sbied 1191 sbequi 1223 ax11indn 1359 r19.21adva 1711 r19.21advva 1714 ralcom2 1768 reu3 1921 sbciegft 1949 reuss2 2265 reupick 2269 ssiun 2582 pwssun 2816 ralxfrd 2887 wefrc 2933 ordelord 2960 tz7.7 2963 onfr 2976 ordtr2 2992 onmindif 3050 unizlim 3103 limsssuc 3111 limomss 3127 findsg 3147 tfinds 3151 tfindsg 3152 funssres 3538 funcnvuni 3550 fv3 3718 funfvima2 3838 isoini 3885 f1oweALT 3891 tfrlem1 3896 tz7.49 3944 abianfp 3947 oarec 4180 omordi 4181 omlimcl 4193 omass 4195 oeordi 4198 oeordsuc 4205 nnmordi 4230 nnaordex 4233 nnawordex 4234 oaabs 4236 omsmolem 4240 eceqopreq 4297 th3qlem1 4298 en3d 4382 xpdom2 4422 sdomen2 4462 mapenlem2 4470 pssnn 4513 suc11reg 4577 inf3lem2 4586 inf3lem5 4589 noinfep 4612 trcl 4617 zfregs 4619 aceq5lem5 4711 zorn2lem4 4763 zorn2lem6 4765 zorn2lem7 4766 fodom 4770 uniimadom 4782 unxpdomlem 4815 alephordi 4846 ltbtwnpq 5056 genpcd 5081 psslinpr 5107 prlem934 5111 ltaddpr 5112 ltexprlem3 5116 ltexprlem6 5119 ltexprlem7 5120 ltapr 5123 prlem936b 5126 prlem936 5127 suplem1pr 5133 suppsr2 5195 suppsr3 5196 ltletrt 5497 xrltletrt 5536 divne0t 5692 lemul12it 5800 divgt0t 5809 divge0t 5810 nnsub 5903 lbreu 5992 sup2 5998 infmrcl 6016 bndndx 6020 xrub 6027 supxrunb2 6037 elnnz 6092 btwnnzt 6139 uzindOLD 6156 uzwo4OLD 6158 uzwo5OLD 6159 zmax 6168 zbtwnre 6169 qbtwnre 6216 ser1add2 6275 ser1add 6276 icounlem 6345 uzwo 6387 uzwoOLD 6388 fzoptht 6434 fzrevralt 6451 le2sqit 6563 sqlecant 6572 sq01t 6582 absrpclt 6790 cau4i 6855 cau5 6856 caubnd 6863 facdivt 6879 facwordit 6881 faclbnd 6882 bccl2t 6909 clm3 7017 2climnn 7039 2climnn0 7040 climshft 7041 climaddlem3 7052 climmullem8 7063 climsqueeze 7076 climsqueeze2 7077 climsup 7091 caucvglem4 7096 caucvglem6 7098 reccnv 7153 cvgratlem1ALT 7182 cvgratlem5 7189 fsum0diag3 7195 fsum0diag4 7196 xpnnen 7441 znnenlemOLD 7444 infpnlem1 7449 infxpidmlem11 7505 uniopnt 7540 basgen2t 7581 subtop 7588 clsval2 7627 neii1 7662 neii2 7663 cncnpi 7712 cncnp 7717 metge0 7760 metxp 7774 ssbl 7795 opnin 7809 metcnp 7826 metcnpi3 7831 metcnpi4 7832 metcni 7833 metcni2 7834 lmnn 7873 metelcls 7900 metcnp4lem2 7903 metcnp4 7904 iscms2lem5 7927 lmcau 7930 cmsss 7931 bcthlem18 7950 bcthlem21 7953 bcthlem28 7960 isgrp2i 8011 grplactf1o 8034 nmoub3i 8368 blocnilem 8395 ipasslem5 8425 ubthlem5 8464 ubthlem14 8473 minvecex 8509 efifolem4 8640 efifolem5 8641 chsscm 9033 ocin 9085 ocnelt 9086 occl 9097 projlem26 9127 spansneleq 9409 spansneleqOLD 9410 spansnsst 9411 elspansn4t 9413 h1datom 9421 osumlem6 9500 spansncv 9514 nmopub2tALT 9750 nmfnleub2t 9766 nmcopexlem6 9871 nmcfnexlem6 9900 nlelch 9909 bra11 9954 hstel2t 10056 cvnbtwnt 10123 spansncv2t 10130 dmdmdt 10137 dmdbr3 10141 dmdbr4 10142 mdsl0 10145 mdexch 10170 cvexchlem 10203 atcv1t 10215 atoml 10217 atcvatlem 10220 atcvat2 10222 irred 10229 atcvat4 10232 mdsymlem3 10240 mdsymlem4 10241 sumdmdi 10249 sumdmdlem 10252 cdj1 10265 cdj3lem1 10266 ghomf1olem 10301 uninqs 10342 oooeqim2 10371 fiiu2 10377 truni1 10386 hmphtr 10418 qusp 10430 fillsb 10435 fipfil2 10439 oefil2 10441 neifil 10442 efilcp 10445 efilcp2 10450 cnfilca 10451 iintlem1 10476 mrdmcd 10566 imonclem 10583 ismonc 10584 cmpmon 10585 icmpmon 10587

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-mp 7

Copyright terms: Public domain