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

Theorem ancom 439
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  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)

Proof of Theorem ancom
StepHypRef Expression
1 pm3.22 438 . 2  |-  ( (
ph  /\  ps )  ->  ( ps  /\  ph ) )
2 pm3.22 438 . 2  |-  ( ( ps  /\  ph )  ->  ( ph  /\  ps ) )
31, 2impbii 182 1  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  ancomd  440  ancomsd  442  pm4.71r  614  pm5.32ri  621  pm5.32rd  623  anbi2ci  679  anbi12ci  681  an12  774  an32  775  an13  776  an42  800  andir  840  dfbi3  865  rbaib  875  rbaibr  876  3anrot  941  3ancoma  943  nancom  1292  excxor  1302  ancomsimp  1361  cador  1383  cadcoma  1387  cadcomb  1388  cad1  1390  exancom  1574  19.42  1817  eu1  2165  moaneu  2203  moanmo  2204  2eu3  2226  2eu6  2229  2eu7  2230  2eu8  2231  eq2tri  2343  r19.28av  2683  r19.29r  2685  r19.42v  2695  rexcomf  2700  rabswap  2720  euxfr2  2951  rmo4  2959  reu8  2962  rmo3  3079  incom  3362  difin2  3431  difin0ss  3521  ssunsn  3775  inuni  4176  eqvinop  4250  dfid3  4309  uniuni  4526  reuxfr2d  4556  elvvv  4748  brinxp2  4750  dmuni  4887  dfres2  5001  dfima2  5013  imadmrn  5023  imai  5026  asymref2  5059  cnvxp  5096  cnvcnvsn  5148  opswap  5157  mptpreima  5164  rnco  5177  ressn  5209  fncnv  5279  fununi  5281  fnres  5325  fnopabg  5332  dff1o2  5442  eqfnfv3  5585  respreima  5615  fsn  5657  fliftcnv  5771  isoini  5796  ndmovcom  5968  brtpos2  6201  brtpos  6204  tpostpos  6215  tposmpt2  6232  tfrlem7  6394  oaord  6540  oeeu  6596  nnaord  6612  pmex  6772  elpmg  6781  mapval2  6792  mapsnen  6933  map1  6934  xpsnen  6941  xpcomco  6947  elfi2  7163  supmo  7198  cp  7556  dfac5lem1  7745  dfac5lem2  7746  dfac5lem3  7747  dfac2  7752  kmlem3  7773  cdacomen  7802  cf0  7872  cflim3  7883  brdom7disj  8151  brdom6disj  8152  recmulnq  8583  letri3  8902  lesub0  9285  wloglei  9300  creur  9735  indstr  10282  xrltlen  10475  xrletri3  10481  qbtwnre  10520  xmulcom  10580  xmulneg1  10583  xmulf  10586  iooneg  10750  iccneg  10751  elfzuzb  10786  fzrev  10840  fzm1  10856  rediv  11610  imdiv  11617  lenegsq  11798  o1lo1  12005  fsumcom2  12231  fsumcom  12232  divalglem10  12595  smueqlem  12675  gcdcom  12693  isprm2  12760  infpn2  12954  imasleval  13437  invsym  13658  subsubc  13721  isffth2  13784  odulatb  14241  oduclatb  14242  resscntz  14801  oppgid  14823  gsumcom  15222  dfrhm2  15492  lsslss  15712  fiidomfld  16043  opsrtoslem1  16219  xrsdsreclb  16412  znleval  16502  istps3OLD  16654  ntreq0  16808  restopn2  16902  ist0-3  17067  1stcelcls  17181  txkgen  17340  trfil2  17576  elflim2  17653  flimrest  17672  txflf  17695  fclsrest  17713  tsmssubm  17819  ismet2  17892  blres  17971  metrest  18064  xrtgioo  18306  elii1  18427  evthicc2  18814  ovolfcl  18820  ovoliunlem1  18855  dyaddisj  18945  mbfaddlem  19009  itg1climres  19063  mbfi1fseqlem4  19067  iblpos  19141  itgposval  19144  ditgsplit  19205  ellimc3  19223  itgsubst  19390  deg1ldg  19472  sincosq1sgn  19860  sincosq3sgn  19862  cos11  19889  dvdsflsumcom  20422  fsumvma  20446  logfaclbnd  20455  dchrelbas3  20471  lgsdi  20565  lgsquadlem1  20587  lgsquadlem2  20588  lgsquadlem3  20589  h2hcau  21551  h2hlm  21552  axhcompl-zf  21570  nmopub  22480  nmfnleub  22497  chrelati  22936  cvexchlem  22940  mdsymlem8  22982  sumdmdii  22987  ballotlem2  23040  eupath2lem2  23306  mulsuble0b  23491  coep  23511  dfpo2  23515  dfdm5  23533  dfrn5  23534  wfi  23608  frind  23644  tfrALTlem  23677  nocvxmin  23746  brtxp  23828  brimg  23883  brcup  23885  brcap  23886  funpartfun  23888  dfrdg4  23895  tfrqfree  23896  cgrcomlr  24028  ofscom  24037  btwnexch  24055  fscgr  24110  eeeeanv  24342  eqvinopb  24363  dff1o6f  24490  cmpdom  24542  dualded  25182  dualcat2  25183  lineval4a  25486  heibor1  25933  isdrngo3  25989  isdmn3  26098  an43OLD  26112  prtlem70  26114  prtlem90  26122  fz1eqin  26247  diophrex  26254  fphpd  26298  fzneg  26468  expdioph  26515  dford4  26521  lnr2i  26719  gsumcom3  26853  fgraphopab  26928  2reu3  27345  2reu7  27348  2reu8  27349  ndmaovcom  27444  uunT1p1  27824  uun132p1  27829  un2122  27833  uun2131p1  27835  uunT12p1  27843  uunT12p2  27844  uunT12p3  27845  uun2221  27856  uun2221p1  27857  uun2221p2  27858  3impdirp1  27859  ancomsimpVD  27909  bnj257  27999  bnj545  28194  bnj594  28211  lrelat  28471  islshpat  28474  atlrelat1  28778  ishlat2  28810  pmapglb  29226  polval2N  29362  cdlemb3  30062  diblsmopel  30628  dicelval3  30637  diclspsn  30651
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator