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

Theorem ancom 437
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 436 . 2  |-  ( (
ph  /\  ps )  ->  ( ps  /\  ph ) )
2 pm3.22 436 . 2  |-  ( ( ps  /\  ph )  ->  ( ph  /\  ps ) )
31, 2impbii 180 1  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  ancomd  438  ancomsd  440  pm4.71r  612  pm5.32ri  619  pm5.32rd  621  anbi2ci  677  anbi12ci  679  an12  772  an32  773  an13  774  an42  798  andir  838  dfbi3  863  rbaib  873  rbaibr  874  3anrot  939  3ancoma  941  nancom  1290  excxor  1300  ancomsimp  1359  cador  1381  cadcoma  1385  cadcomb  1386  cad1  1388  exancom  1576  19.42  1828  eu1  2177  moaneu  2215  moanmo  2216  2eu3  2238  2eu6  2241  2eu7  2242  2eu8  2243  eq2tri  2355  r19.28av  2695  r19.29r  2697  r19.42v  2707  rexcomf  2712  rabswap  2732  euxfr2  2963  rmo4  2971  reu8  2974  rmo3  3091  incom  3374  difin2  3443  difin0ss  3533  ssunsn  3790  inuni  4189  eqvinop  4267  dfid3  4326  uniuni  4543  reuxfr2d  4573  elvvv  4765  brinxp2  4767  dmuni  4904  dfres2  5018  dfima2  5030  imadmrn  5040  imai  5043  asymref2  5076  cnvxp  5113  cnvcnvsn  5166  opswap  5175  mptpreima  5182  rnco  5195  ressn  5227  fncnv  5330  fununi  5332  fnres  5376  fnopabg  5383  dff1o2  5493  eqfnfv3  5640  respreima  5670  fsn  5712  fliftcnv  5826  isoini  5851  ndmovcom  6023  brtpos2  6256  brtpos  6259  tpostpos  6270  tposmpt2  6287  tfrlem7  6415  oaord  6561  oeeu  6617  nnaord  6633  pmex  6793  elpmg  6802  mapval2  6813  mapsnen  6954  map1  6955  xpsnen  6962  xpcomco  6968  elfi2  7184  supmo  7219  cp  7577  dfac5lem1  7766  dfac5lem2  7767  dfac5lem3  7768  dfac2  7773  kmlem3  7794  cdacomen  7823  cf0  7893  cflim3  7904  brdom7disj  8172  brdom6disj  8173  recmulnq  8604  letri3  8923  lesub0  9306  wloglei  9321  creur  9756  indstr  10303  xrltlen  10496  xrletri3  10502  qbtwnre  10542  xmulcom  10602  xmulneg1  10605  xmulf  10608  iooneg  10772  iccneg  10773  elfzuzb  10808  fzrev  10862  fzm1  10878  rediv  11632  imdiv  11639  lenegsq  11820  o1lo1  12027  fsumcom2  12253  fsumcom  12254  divalglem10  12617  smueqlem  12697  gcdcom  12715  isprm2  12782  infpn2  12976  imasleval  13459  invsym  13680  subsubc  13743  isffth2  13806  odulatb  14263  oduclatb  14264  resscntz  14823  oppgid  14845  gsumcom  15244  dfrhm2  15514  lsslss  15734  fiidomfld  16065  opsrtoslem1  16241  xrsdsreclb  16434  znleval  16524  istps3OLD  16676  ntreq0  16830  restopn2  16924  ist0-3  17089  1stcelcls  17203  txkgen  17362  trfil2  17598  elflim2  17675  flimrest  17694  txflf  17717  fclsrest  17735  tsmssubm  17841  ismet2  17914  blres  17993  metrest  18086  xrtgioo  18328  elii1  18449  evthicc2  18836  ovolfcl  18842  ovoliunlem1  18877  dyaddisj  18967  mbfaddlem  19031  itg1climres  19085  mbfi1fseqlem4  19089  iblpos  19163  itgposval  19166  ditgsplit  19227  ellimc3  19245  itgsubst  19412  deg1ldg  19494  sincosq1sgn  19882  sincosq3sgn  19884  cos11  19911  dvdsflsumcom  20444  fsumvma  20468  logfaclbnd  20477  dchrelbas3  20493  lgsdi  20587  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  h2hcau  21575  h2hlm  21576  axhcompl-zf  21594  nmopub  22504  nmfnleub  22521  chrelati  22960  cvexchlem  22964  mdsymlem8  23006  sumdmdii  23011  ballotlem2  23063  reuxfr3d  23154  iuninc  23174  rmo3f  23194  rmo4fOLD  23195  mptfnf  23241  xrofsup  23270  cnvordtrestixx  23312  xrsinvgval  23321  xrsmulgzz  23322  issgon  23499  isibfm  23608  eupath2lem2  23917  mulsuble0b  24103  coep  24179  dfpo2  24183  dfdm5  24203  dfrn5  24204  wfi  24278  frind  24314  tfrALTlem  24347  nocvxmin  24416  brtxp  24491  dffun10  24524  brimg  24547  brcup  24549  brcap  24550  funpartfun  24553  dfrdg4  24560  tfrqfree  24561  cgrcomlr  24693  ofscom  24702  btwnexch  24720  fscgr  24775  eeeeanv  25047  eqvinopb  25068  dff1o6f  25195  cmpdom  25246  dualded  25886  dualcat2  25887  lineval4a  26190  heibor1  26637  isdrngo3  26693  isdmn3  26802  an43OLD  26816  prtlem70  26818  prtlem90  26826  fz1eqin  26951  diophrex  26958  fphpd  27002  fzneg  27172  expdioph  27219  dford4  27225  lnr2i  27423  gsumcom3  27557  fgraphopab  27632  2reu3  28069  2reu7  28072  2reu8  28073  ndmaovcom  28173  jaoi2  28176  injresinj  28215  cusgra3v  28299  trls  28335  trlon  28339  istrlon  28340  pthon  28361  3v3e3cycl2  28410  uunT1p1  28870  uun132p1  28875  un2122  28879  uun2131p1  28881  uunT12p1  28889  uunT12p2  28890  uunT12p3  28891  uun2221  28902  uun2221p1  28903  uun2221p2  28904  3impdirp1  28905  ancomsimpVD  28957  bnj257  29048  bnj545  29243  bnj594  29260  lrelat  29826  islshpat  29829  atlrelat1  30133  ishlat2  30165  pmapglb  30581  polval2N  30717  cdlemb3  31417  diblsmopel  31983  dicelval3  31992  diclspsn  32006
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator