| 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 | simpr 350 |
. . 3
| |
| 2 | simpl 346 |
. . 3
| |
| 3 | 1, 2 | jca 310 |
. 2
|
| 4 | simpr 350 |
. . 3
| |
| 5 | simpl 346 |
. . 3
| |
| 6 | 4, 5 | jca 310 |
. 2
|
| 7 | 3, 6 | impbii 174 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: ancomd 483 ancoms 484 ancomsd 485 pm3.22 486 anbi1i 539 an12 542 an23 543 anabs5 551 an42 565 bicom 579 andir 666 anbi1d 679 pm4.71r 698 pm5.32ri 708 pm5.32rd 710 xor 734 xor2 736 biantrurdOLD 797 consensusOLD 845 rnlemOLD 854 3anrot 863 3ancoma 865 ancomsimp 1291 exancom 1401 19.29r 1423 19.42 1450 exanOLD 1464 eu1 1786 mooran1OLD 1823 moaneu 1830 moanmo 1831 2eu3 1855 2eu6 1858 2eu7 1859 2eu8 1860 eq2tri 1956 clabel 2014 r19.28av 2226 r19.29r 2229 r19.42v 2237 ralcom 2242 rexcom 2243 rabswap 2256 gencbvexOLD 2335 euxfr2 2437 euind 2439 rmo4 2445 reu8 2448 reuind 2450 incom 2787 symdif2OLD 2858 difin0ss 2939 inuni 3470 moabex 3513 eqvinop 3536 opelopabsb 3564 dfid3 3587 ordtri4OLD 3700 uniuni 3806 reuxfr2d 3844 reuxfr2 3845 ordpwsuc 3896 elxp2 4019 elvvv 4054 cnvcoOLD 4146 dmuni 4166 opres 4225 dfima2 4265 dfima2OLD 4266 imadmrn 4277 imai 4280 asymref 4308 asymrefOLD 4309 asymref2 4310 intirrOLD 4313 rnuni 4327 cnvxp 4332 cnvxpOLD 4333 rninxpOLD 4356 cnvsn 4373 coresOLD 4401 rnco 4404 cnvpo 4427 fncnv 4479 fununi 4481 funinOLD 4485 f1cnv 4611 dff1o2 4639 tz6.12-1 4693 eqfnfv3 4769 fsn 4807 isoini 4877 ndmoprcom 4980 fparlem1 5081 fparlem2 5082 fsplit 5086 reiota4 5107 tfrlem7 5125 oaord 5228 uniqs 5354 pmex 5386 mapval2 5394 mapsnen 5488 map1 5489 xpsnen 5494 xpcomen 5498 pw2en 5505 ordiso 5683 cp 5852 aceq5lem1 5897 aceq5lem2 5898 aceq5lem3 5899 aceq6b 5904 kmlem3 5929 brdom7disj 5966 brdom6disj 5967 cf0 6058 genpass 6264 1pr 6269 addcompr 6275 mulcompr 6277 reclem2pr 6309 elreal 6402 ltxr 6664 letri3 6687 lesub0i 6792 lesub0iOLD 6793 addgtge0OLD 6836 iooneg 7575 iccneg 7576 icounlem 7581 indstr 7630 elfzuzb 7646 elfzuz2 7656 fzrev 7689 lenegsq 8137 cau5i 8171 sumex 8241 clm4i 8340 infpn2 8778 infxpidmlem9 8829 istps3 8877 tgval3 8895 tgss3 8908 clsval2 8961 metxp 9111 issubg 9425 sincosq1sgn 10053 sincosq2sgn 10054 sincosq3sgn 10055 sincosq4sgn 10056 exidu1 10373 grpmnd 10393 h2hcau 10481 shorth 10801 5oalem2 11235 3oalem2 11243 mdsldmd1i 11903 chrelati 11936 cvexchlem 11940 mdsymlem8 11982 sumdmdii 11987 bnj170OLD 12035 bnj171OLD 12037 bnj172OLD 12039 bnj173OLD 12041 bnj174OLD 12043 bnj176OLD 12046 bnj177 12047 bnj178 12048 bnj179OLD 12050 bnj182 12053 bnj184OLD 12055 bnj186 12056 bnj257 12096 bnj345OLD 12188 bnj367OLD 12211 bnj32OLD 12399 bnj50OLD 12425 bnj112 12457 bnj134 12478 bnj163OLD 12490 bnj876 12803 bnj878 12805 bnj1370 13094 imim21b 13597 divalglem10 13705 gcdcom 13726 mulgcdlem2 13757 isprm2 13775 dffr5 13831 tz6.26 13913 wfi 13915 frind 13939 soxp 13950 wfrlem5 13961 tfrALTlem 13976 nocvxmin 14029 axfelem14 14044 eeeeanv 14272 excxor 14280 cmpdom 14481 prodex 14656 rcfpfillem3 14930 letri31 15019 homib 15145 settrcon 15247 trer 15361 fictb 15371 ordisoOLD 15374 is1stc3 15469 ist0-2 15539 difin2 15676 respreima 15684 eqfnfv3OLD 15721 fzsplit 15792 fzm1 15796 sstotbnd 15936 heiborlem1 15955 exidresid 16032 isdivrng3 16112 isdmn3 16222 an43OLD 16236 prtlem70 16238 prtlem90 16246 prter1 16282 ancomsimpVD 16689 strdif 16719 posgelem 16795 hlrelat1 17049 pmapglb 17252 polval2 17319 |
| 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 164 df-an 242 |