MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancom Unicode version

Theorem ancom 450
Description: Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.)
Assertion
Ref Expression
ancom

Proof of Theorem ancom
StepHypRef Expression
1 pm3.22 449 . 2
2 pm3.22 449 . 2
31, 2impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  ancomd  451  ancomst  452  ancomsd  454  pm4.71r  631  pm5.32ri  638  pm5.32rd  640  anbi2ci  696  anbi12ci  698  an12  797  an32  798  an13  799  an42  825  andir  868  dfbi3  893  rbaibOLD  907  rbaibrOLD  908  3anrot  978  3ancoma  980  nancom  1346  nancomOLD  1347  excxor  1368  dfifp6  1386  cador  1458  cadcoma  1462  cadcomb  1463  cad1  1465  exancom  1671  19.42v  1775  19.42  1972  sbel2x  2203  moanmo  2353  2eu3  2379  2eu6OLD  2384  2eu7  2385  2eu8  2386  eq2tri  2525  r19.28v  2991  r19.29r  2993  r19.42v  3012  rexcomf  3017  rabswap  3037  euxfr2  3284  rmo4  3292  reu8  3295  rmo3  3429  incom  3690  difin2  3759  difin0ss  3894  ssunsn  4190  inuni  4614  reuxfr2d  4675  eqvinop  4736  dfid3  4801  elvvv  5064  brinxp2  5066  dmuni  5217  dfres2  5331  dfima2  5344  imadmrn  5352  imai  5354  asymref2  5389  cnvxp  5429  xpdifid  5440  cnvcnvsn  5490  opswap  5500  mptpreima  5505  rnco  5518  ressn  5548  xpco  5552  fncnv  5657  fununi  5659  fnres  5702  fnopabg  5709  dff1o2  5826  eqfnfv3  5983  respreima  6016  fsn  6069  f13dfv  6180  fliftcnv  6209  isoini  6234  elrnmpt2res  6416  ndmovcom  6462  uniuni  6609  brtpos2  6980  brtpos  6983  tpostpos  6994  tposmpt2  7011  mpt2curryd  7017  oaord  7215  oeeu  7271  nnaord  7287  pmex  7444  elpmg  7454  mapval2  7468  mapsnen  7613  map1  7614  xpsnen  7621  xpcomco  7627  elfi2  7894  supmo  7932  cp  8330  dfac5lem1  8525  dfac5lem2  8526  dfac5lem3  8527  dfac2  8532  kmlem3  8553  cdacomen  8582  cf0  8652  cflim3  8663  brdom7disj  8930  brdom6disj  8931  recmulnq  9363  letri3  9691  lesub0  10094  wloglei  10110  mulsuble0b  10439  creur  10555  indstr  11179  xrltlen  11381  xrletri3  11387  qbtwnre  11427  xmulcom  11487  xmulneg1  11490  xmulf  11493  iooneg  11669  iccneg  11670  elfzuzb  11711  fzrev  11771  ssfzoulel  11906  injresinj  11926  wrdeqswrdlsw  12674  rediv  12964  imdiv  12971  lenegsq  13153  o1lo1  13360  fsumcom2  13589  fsumcom  13590  fprodcom2  13788  fprodcom  13789  divalglem10  14060  smueqlem  14140  gcdcom  14158  isprm2  14225  infpn2  14431  imasleval  14938  invsym  15156  subsubc  15222  isffth2  15285  odulatb  15773  oduclatb  15774  posglbmo  15777  resscntz  16369  oppgid  16391  gsumcom  17005  dfrhm2  17366  lsslss  17607  fiidomfld  17957  opsrtoslem1  18148  xrsdsreclb  18465  znleval  18593  gsumcom3  18901  madutpos  19144  fvmptnn04if  19350  istps3OLD  19423  ntreq0  19578  restopn2  19678  ist0-3  19846  1stcelcls  19962  txkgen  20153  trfil2  20388  elflim2  20465  flimrest  20484  txflf  20507  fclsrest  20525  tsmssubm  20644  ismet2  20836  blres  20934  metrest  21027  restmetu  21090  xrtgioo  21311  elii1  21435  evthicc2  21872  ovolfcl  21878  ovoliunlem1  21913  dyaddisj  22005  mbfaddlem  22067  itg1climres  22121  mbfi1fseqlem4  22125  iblpos  22199  itgposval  22202  ditgsplit  22265  ellimc3  22283  itgsubst  22450  deg1ldg  22492  sincosq1sgn  22891  sincosq3sgn  22893  cos11  22920  dvdsflsumcom  23464  fsumvma  23488  logfaclbnd  23497  dchrelbas3  23513  lgsdi  23607  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  istrkg2ld  23858  mirreu3  24035  hpgcom  24136  cusgra3v  24464  trls  24538  trlon  24542  pthon  24577  spthon  24584  3v3e3cycl2  24664  clwwlkn2  24775  usg2spthonot0  24889  rusgranumwlkl1  24947  rusgra0edg  24955  eupath2lem2  24978  frg2wot1  25057  frg2woteqm  25059  usg2spot2nb  25065  usgreg2spot  25067  frgrareg  25117  frgraregord013  25118  h2hcau  25896  h2hlm  25897  axhcompl-zf  25915  nmopub  26827  nmfnleub  26844  chrelati  27283  cvexchlem  27287  mdsymlem8  27329  sumdmdii  27334  spc2ed  27372  reuxfr3d  27388  rmo3f  27394  rmo4fOLD  27395  mptfnf  27499  2ndpreima  27525  fpwrelmapffslem  27555  xrofsup  27582  cnvordtrestixx  27895  issgon  28123  eulerpartlemr  28313  eulerpartlemgvv  28315  ballotlem2  28427  sgn3da  28480  coep  29180  dfpo2  29184  dfdm5  29206  dfrn5  29207  elima4  29209  wfi  29287  frind  29323  nocvxmin  29451  brtxp  29530  elfix  29553  dffix2  29555  sscoid  29563  brimg  29587  funpartfun  29593  dfrdg4  29600  tfrqfree  29601  cgrcomlr  29648  ofscom  29657  btwnexch  29675  fscgr  29730  wl-ax11-lem4  30028  fin2solem  30039  ftc1anclem6  30095  ftc1anc  30098  heibor1  30306  isdrngo3  30362  isdmn3  30471  an43OLD  30590  prtlem70  30592  prtlem90  30598  fz1eqin  30702  diophrex  30709  fphpd  30750  fzneg  30920  expdioph  30965  dford4  30971  lnr2i  31065  fgraphopab  31170  isprm7  31192  lcmcom  31199  icccncfext  31690  dvnmul  31740  dvmptfprodlem  31741  dvnprodlem2  31744  fourierdlem42  31931  fourierdlem83  31972  2reu3  32193  2reu7  32196  2reu8  32197  ndmaovcom  32290  usgra2pth0  32355  euelss  32553  dfiso3  32569  2zrngnmrid  32756  opeliun2xp  32922  eliunxp2  32923  uunT1p1  33578  uun132p1  33583  un2122  33587  uun2131p1  33589  uunT12p1  33597  uunT12p2  33598  uunT12p3  33599  uun2221  33610  uun2221p1  33611  uun2221p2  33612  3impdirp1  33613  ancomstVD  33665  bnj257  33759  bnj545  33953  bnj594  33970  bj-dfifc2  34164  bj-eldiag  34606  bj-ccinftydisj  34616  lrelat  34739  islshpat  34742  atlrelat1  35046  ishlat2  35078  pmapglb  35494  polval2N  35630  cdlemb3  36332  diblsmopel  36898  dicelval3  36907  diclspsn  36921  bj-ifidg  37707  bj-ifid1g  37708  bj-ifid2g  37709  bj-if1bi  37720  bj-ifdfbi  37730  rp-fakeoranass  37738  xpcogend  37773
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 185  df-an 371
  Copyright terms: Public domain W3C validator