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  2137  moaneu  2175  moanmo  2176  2eu3  2198  2eu6  2201  2eu7  2202  2eu8  2203  eq2tri  2315  r19.28av  2655  r19.29r  2657  r19.42v  2667  rexcomf  2672  rabswap  2692  euxfr2  2918  rmo4  2926  reu8  2929  rmo3  3039  incom  3322  difin2  3391  difin0ss  3481  ssunsn  3734  inuni  4135  eqvinop  4209  dfid3  4268  uniuni  4485  reuxfr2d  4515  elvvv  4723  brinxp2  4725  dmuni  4862  dfres2  4976  dfima2  4988  imadmrn  4998  imai  5001  asymref2  5034  cnvxp  5071  cnvcnvsn  5123  opswap  5132  mptpreima  5139  rnco  5152  ressn  5184  fncnv  5238  fununi  5240  fnres  5284  fnopabg  5291  dff1o2  5401  eqfnfv3  5544  respreima  5574  fsn  5616  fliftcnv  5730  isoini  5755  ndmovcom  5927  brtpos2  6160  brtpos  6163  tpostpos  6174  tposmpt2  6191  tfrlem7  6353  oaord  6499  oeeu  6555  nnaord  6571  pmex  6731  elpmg  6740  mapval2  6751  mapsnen  6892  map1  6893  xpsnen  6900  xpcomco  6906  elfi2  7122  supmo  7157  cp  7515  dfac5lem1  7704  dfac5lem2  7705  dfac5lem3  7706  dfac2  7711  kmlem3  7732  cdacomen  7761  cf0  7831  cflim3  7842  brdom7disj  8110  brdom6disj  8111  recmulnq  8542  letri3  8861  lesub0  9244  wloglei  9259  creur  9694  indstr  10240  xrltlen  10433  xrletri3  10439  qbtwnre  10478  xmulcom  10538  xmulneg1  10541  xmulf  10544  iooneg  10708  iccneg  10709  elfzuzb  10744  fzrev  10798  fzm1  10814  rediv  11567  imdiv  11574  lenegsq  11755  o1lo1  11962  fsumcom2  12188  fsumcom  12189  divalglem10  12549  smueqlem  12629  gcdcom  12647  isprm2  12714  infpn2  12908  imasleval  13391  invsym  13612  subsubc  13675  isffth2  13738  odulatb  14195  oduclatb  14196  resscntz  14755  oppgid  14777  gsumcom  15176  dfrhm2  15446  lsslss  15666  fiidomfld  15997  opsrtoslem1  16173  xrsdsreclb  16366  znleval  16456  istps3OLD  16608  ntreq0  16762  restopn2  16856  ist0-3  17021  1stcelcls  17135  txkgen  17294  trfil2  17530  elflim2  17607  flimrest  17626  txflf  17649  fclsrest  17667  tsmssubm  17773  ismet2  17846  blres  17925  metrest  18018  xrtgioo  18260  elii1  18381  evthicc2  18768  ovolfcl  18774  ovoliunlem1  18809  dyaddisj  18899  mbfaddlem  18963  itg1climres  19017  mbfi1fseqlem4  19021  iblpos  19095  itgposval  19098  ditgsplit  19159  ellimc3  19177  itgsubst  19344  deg1ldg  19426  sincosq1sgn  19814  sincosq3sgn  19816  cos11  19843  dvdsflsumcom  20376  fsumvma  20400  logfaclbnd  20409  dchrelbas3  20425  lgsdi  20519  lgsquadlem1  20541  lgsquadlem2  20542  lgsquadlem3  20543  h2hcau  21505  h2hlm  21506  axhcompl-zf  21524  nmopub  22434  nmfnleub  22451  chrelati  22890  cvexchlem  22894  mdsymlem8  22936  sumdmdii  22941  ballotlem2  22994  eupath2lem2  23260  mulsuble0b  23445  coep  23465  dfpo2  23469  dfdm5  23487  dfrn5  23488  wfi  23562  frind  23598  tfrALTlem  23631  nocvxmin  23700  brtxp  23782  brimg  23837  brcup  23839  brcap  23840  funpartfun  23842  dfrdg4  23849  tfrqfree  23850  cgrcomlr  23982  ofscom  23991  btwnexch  24009  fscgr  24064  eeeeanv  24296  eqvinopb  24317  dff1o6f  24444  cmpdom  24496  dualded  25136  dualcat2  25137  lineval4a  25440  heibor1  25887  isdrngo3  25943  isdmn3  26052  an43OLD  26066  prtlem70  26068  prtlem90  26076  fz1eqin  26201  diophrex  26208  fphpd  26252  fzneg  26422  expdioph  26469  dford4  26475  lnr2i  26673  gsumcom3  26807  fgraphopab  26882  uunT1p1  27590  uun132p1  27595  un2122  27599  uun2131p1  27601  uunT12p1  27609  uunT12p2  27610  uunT12p3  27611  uun2221  27622  uun2221p1  27623  uun2221p2  27624  3impdirp1  27625  ancomsimpVD  27675  bnj257  27765  bnj545  27960  bnj594  27977  lrelat  28355  islshpat  28358  atlrelat1  28662  ishlat2  28694  pmapglb  29110  polval2N  29246  cdlemb3  29946  diblsmopel  30512  dicelval3  30521  diclspsn  30535
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