| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. |
| Ref | Expression |
|---|---|
| ancom |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm3.27 330 |
. . 3
| |
| 2 | pm3.26 326 |
. . 3
| |
| 3 | 1, 2 | jca 295 |
. 2
|
| 4 | pm3.27 330 |
. . 3
| |
| 5 | pm3.26 326 |
. . 3
| |
| 6 | 4, 5 | jca 295 |
. 2
|
| 7 | 3, 6 | impbii 164 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: ancoms 447 ancomsd 448 pm3.22 449 anbi1i 492 an12 495 an23 496 anabs5 504 an42 518 bicom 531 andir 616 anbi1d 628 pm4.71r 647 pm5.32ri 657 pm5.32rd 659 xor 682 xor2 684 biantrurd 739 consensus 779 rnlem 785 3anrot 792 3ancoma 794 exancom 1095 19.29r 1113 19.42 1137 exan 1147 eu1 1434 mooran1 1467 moaneu 1472 moanmo 1473 2eu3 1494 2eu6 1497 2eu7 1498 2eu8 1499 eq2tri 1580 clabel 1629 r19.28av 1802 r19.29r 1804 r19.42v 1811 rabswap 1818 ralcom 1821 rexcom 1822 gencbvex 1885 euxfr2 1973 rmo4 1980 reu8 1983 incom 2259 symdif2 2317 difin0ss 2384 iunid 2657 moabex 2822 eqvinop 2847 dfid3 2892 uniuni 2937 reuxfr2 2960 ordtri4 3041 ordpwsuc 3123 elxp2 3260 cnvco 3357 dmuni 3376 dfima2 3462 imadmrn 3471 imai 3474 asymref 3496 intirr 3498 cnvsn 3506 rnuni 3516 cnvxp 3521 rninxp 3539 cores 3556 rnco 3559 cnvpo 3579 fncnv 3618 fununi 3620 funin 3623 f1cnv 3723 tz6.12-1 3793 fsn 3891 isoini 3958 tfrlem7 3975 ndmoprcom 4105 2ndconst 4155 oaord 4239 uniqs 4356 pmex 4388 mapval2 4396 mapsnen 4490 map1 4491 xpsnen 4498 xpcomen 4502 pw2en 4509 mapxpen 4560 cp 4784 aceq5lem1 4797 aceq5lem2 4798 aceq5lem3 4799 aceq6b 4804 kmlem3 4829 brdom7disj 4866 brdom6disj 4867 cf0 4975 genpass 5177 1pr 5182 addcompr 5188 mulcompr 5190 reclem2pr 5222 elreal 5315 ltxr 5560 letri3 5582 lesub0i 5677 addgtge0 5714 divmul13 5840 divmul24 5841 divdivdiv 5843 iooneg 6432 iccneg 6433 icounlem 6438 indstr 6487 elfzuzb 6502 elfzuz2 6512 fzrev 6537 lenegsq 6975 cau5i 7009 sumex 7071 clm4i 7170 sinbnd 7557 cosbnd 7558 infpn2 7601 infxpidmlem9 7652 istps3 7699 tgval3 7714 tgss3 7727 clsval2 7770 metxp 7919 issubg 8200 sincosq1sgn 8787 sincosq2sgn 8788 sincosq3sgn 8789 sincosq4sgn 8790 h2hcau 8932 shorth 9251 5oalem2 9683 3oalem2 9691 mdsldmd1i 10342 chrelati 10375 cvexchlem 10379 mdsymlem8 10421 sumdmdii 10426 eeeeanv 10522 ntunte 10525 cmpdom 10549 rcfpfillem3 10673 homib 10806 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 |
| This theorem depends on definitions: df-bi 154 df-an 232 |