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  615  pm5.32ri  622  pm5.32rd  624  anbi2ci  680  anbi12ci  682  an12  775  an32  776  an13  777  an42  801  andir  843  dfbi3  868  rbaib  878  rbaibr  879  3anrot  944  3ancoma  946  nancom  1295  excxor  1305  ancomsimp  1365  cador  1387  cadcoma  1391  cadcomb  1392  cad1  1394  exancom  1584  19.42  1800  eu1  2134  moaneu  2172  moanmo  2173  2eu3  2195  2eu6  2198  2eu7  2199  2eu8  2200  eq2tri  2312  r19.28av  2644  r19.29r  2646  r19.42v  2656  rexcomf  2661  rabswap  2678  euxfr2  2887  rmo4  2897  reu8  2900  rmo3  3006  incom  3269  difin2  3337  difin0ss  3426  ssunsn  3674  inuni  4071  eqvinop  4144  dfid3  4203  uniuni  4418  reuxfr2d  4448  elvvv  4656  brinxp2  4658  dmuni  4795  dfres2  4909  dfima2  4921  imadmrn  4931  imai  4934  asymref2  4967  cnvxp  5004  cnvcnvsn  5056  opswap  5065  mptpreima  5072  rnco  5085  ressn  5117  fncnv  5171  fununi  5173  fnres  5217  fnopabg  5224  dff1o2  5334  eqfnfv3  5476  respreima  5506  fsn  5548  fliftcnv  5662  isoini  5687  ndmovcom  5859  brtpos2  6092  brtpos  6095  tpostpos  6106  tposmpt2  6123  tfrlem7  6285  oaord  6431  oeeu  6487  nnaord  6503  pmex  6663  elpmg  6672  mapval2  6683  mapsnen  6823  map1  6824  xpsnen  6831  xpcomco  6837  elfi2  7052  supmo  7087  cp  7445  dfac5lem1  7634  dfac5lem2  7635  dfac5lem3  7636  dfac2  7641  kmlem3  7662  cdacomen  7691  cf0  7761  cflim3  7772  brdom7disj  8040  brdom6disj  8041  recmulnq  8468  letri3  8787  lesub0  9170  wloglei  9185  creur  9620  indstr  10166  xrltlen  10359  xrletri3  10365  qbtwnre  10404  xmulcom  10464  xmulneg1  10467  xmulf  10470  iooneg  10634  iccneg  10635  elfzuzb  10670  fzrev  10724  fzm1  10740  rediv  11493  imdiv  11500  lenegsq  11681  o1lo1  11888  fsumcom2  12114  fsumcom  12115  divalglem10  12475  smueqlem  12555  gcdcom  12573  isprm2  12640  infpn2  12834  imasleval  13317  invsym  13508  subsubc  13571  isffth2  13634  odulatb  14091  oduclatb  14092  resscntz  14642  oppgid  14664  gsumcom  15063  dfrhm2  15333  lsslss  15553  fiidomfld  15881  opsrtoslem1  16057  xrsdsreclb  16250  znleval  16340  istps3OLD  16492  ntreq0  16646  restopn2  16740  ist0-3  16905  1stcelcls  17019  txkgen  17178  trfil2  17414  elflim2  17491  flimrest  17510  txflf  17533  fclsrest  17551  tsmssubm  17657  ismet2  17730  blres  17809  metrest  17902  xrtgioo  18144  elii1  18265  evthicc2  18652  ovolfcl  18658  ovoliunlem1  18693  dyaddisj  18783  mbfaddlem  18847  itg1climres  18901  mbfi1fseqlem4  18905  iblpos  18979  itgposval  18982  ditgsplit  19043  ellimc3  19061  itgsubst  19228  deg1ldg  19310  sincosq1sgn  19698  sincosq3sgn  19700  cos11  19727  dvdsflsumcom  20260  fsumvma  20284  logfaclbnd  20293  dchrelbas3  20309  lgsdi  20403  lgsquadlem1  20425  lgsquadlem2  20426  lgsquadlem3  20427  h2hcau  21389  h2hlm  21390  axhcompl-zf  21408  nmopub  22318  nmfnleub  22335  chrelati  22774  cvexchlem  22778  mdsymlem8  22820  sumdmdii  22825  eupath2lem2  23073  mulsuble0b  23258  coep  23278  dfpo2  23282  dfdm5  23300  dfrn5  23301  wfi  23375  frind  23411  tfrALTlem  23444  nocvxmin  23513  brtxp  23595  brimg  23650  brcup  23652  brcap  23653  funpartfun  23655  dfrdg4  23662  tfrqfree  23663  cgrcomlr  23795  ofscom  23804  btwnexch  23822  fscgr  23877  eeeeanv  24109  eqvinopb  24130  dff1o6f  24257  cmpdom  24309  dualded  24949  dualcat2  24950  lineval4a  25253  heibor1  25700  isdrngo3  25756  isdmn3  25865  an43OLD  25879  prtlem70  25881  prtlem90  25889  fz1eqin  26014  diophrex  26021  fphpd  26065  fzneg  26235  expdioph  26282  dford4  26288  lnr2i  26486  gsumcom3  26620  fgraphopab  26695  uunT1p1  27343  uun132p1  27348  un2122  27352  uun2131p1  27354  uunT12p1  27362  uunT12p2  27363  uunT12p3  27364  uun2221  27375  uun2221p1  27376  uun2221p2  27377  3impdirp1  27378  ancomsimpVD  27428  bnj257  27518  bnj545  27713  bnj594  27730  lrelat  28108  islshpat  28111  atlrelat1  28415  ishlat2  28447  pmapglb  28863  polval2N  28999  cdlemb3  29699  diblsmopel  30265  dicelval3  30274  diclspsn  30288
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