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

Theorem ancom 438
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 437 . 2  |-  ( (
ph  /\  ps )  ->  ( ps  /\  ph ) )
2 pm3.22 437 . 2  |-  ( ( ps  /\  ph )  ->  ( ph  /\  ps ) )
31, 2impbii 181 1  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  ancomd  439  ancomsd  441  pm4.71r  613  pm5.32ri  620  pm5.32rd  622  anbi2ci  678  anbi12ci  680  an12  773  an32  774  an13  775  an42  799  andir  839  dfbi3  864  rbaib  874  rbaibr  875  jaoi2  934  3anrot  941  3ancoma  943  nancom  1299  excxor  1318  ancomsimp  1378  cador  1400  cadcoma  1404  cadcomb  1405  cad1  1407  exancom  1596  19.42  1902  eu1  2301  moaneu  2339  moanmo  2340  2eu3  2362  2eu6  2365  2eu7  2366  2eu8  2367  eq2tri  2494  r19.28av  2837  r19.29r  2839  r19.42v  2854  rexcomf  2859  rabswap  2879  euxfr2  3111  rmo4  3119  reu8  3122  rmo3  3240  incom  3525  difin2  3595  difin0ss  3686  ssunsn  3951  inuni  4354  eqvinop  4433  dfid3  4491  uniuni  4707  reuxfr2d  4737  elvvv  4928  brinxp2  4930  dmuni  5070  dfres2  5184  dfima2  5196  imadmrn  5206  imai  5209  asymref2  5242  cnvxp  5281  cnvcnvsn  5338  opswap  5347  mptpreima  5354  rnco  5367  ressn  5399  xpco  5405  fncnv  5506  fununi  5508  fnres  5552  fnopabg  5559  dff1o2  5670  eqfnfv3  5820  respreima  5850  fsn  5897  fliftcnv  6024  isoini  6049  ndmovcom  6225  brtpos2  6476  brtpos  6479  tpostpos  6490  tposmpt2  6507  tfrlem7  6635  oaord  6781  oeeu  6837  nnaord  6853  pmex  7014  elpmg  7023  mapval2  7034  mapsnen  7175  map1  7176  xpsnen  7183  xpcomco  7189  elfi2  7410  supmo  7446  cp  7804  dfac5lem1  7993  dfac5lem2  7994  dfac5lem3  7995  dfac2  8000  kmlem3  8021  cdacomen  8050  cf0  8120  cflim3  8131  brdom7disj  8398  brdom6disj  8399  recmulnq  8830  letri3  9149  lesub0  9533  wloglei  9548  creur  9983  indstr  10534  xrltlen  10728  xrletri3  10734  qbtwnre  10774  xmulcom  10834  xmulneg1  10837  xmulf  10840  iooneg  11006  iccneg  11007  elfzuzb  11042  fzrev  11097  fzm1  11115  injresinj  11188  rediv  11924  imdiv  11931  lenegsq  12112  o1lo1  12319  fsumcom2  12546  fsumcom  12547  divalglem10  12910  smueqlem  12990  gcdcom  13008  isprm2  13075  infpn2  13269  imasleval  13754  invsym  13975  subsubc  14038  isffth2  14101  odulatb  14558  oduclatb  14559  resscntz  15118  oppgid  15140  gsumcom  15539  dfrhm2  15809  lsslss  16025  fiidomfld  16356  opsrtoslem1  16532  xrsdsreclb  16733  znleval  16823  istps3OLD  16975  ntreq0  17129  restopn2  17229  ist0-3  17397  1stcelcls  17512  txkgen  17672  trfil2  17907  elflim2  17984  flimrest  18003  txflf  18026  fclsrest  18044  tsmssubm  18160  ismet2  18351  blres  18449  metrest  18542  restmetu  18605  xrtgioo  18825  elii1  18948  evthicc2  19345  ovolfcl  19351  ovoliunlem1  19386  dyaddisj  19476  mbfaddlem  19540  itg1climres  19594  mbfi1fseqlem4  19598  iblpos  19672  itgposval  19675  ditgsplit  19736  ellimc3  19754  itgsubst  19921  deg1ldg  20003  sincosq1sgn  20394  sincosq3sgn  20396  cos11  20423  dvdsflsumcom  20961  fsumvma  20985  logfaclbnd  20994  dchrelbas3  21010  lgsdi  21104  lgsquadlem1  21126  lgsquadlem2  21127  lgsquadlem3  21128  cusgra3v  21461  trls  21524  trlon  21528  pthon  21563  spthon  21570  3v3e3cycl2  21639  eupath2lem2  21688  h2hcau  22470  h2hlm  22471  axhcompl-zf  22489  nmopub  23399  nmfnleub  23416  chrelati  23855  cvexchlem  23859  mdsymlem8  23901  sumdmdii  23906  reuxfr3d  23964  rmo3f  23970  rmo4fOLD  23971  mptfnf  24061  2ndpreima  24084  xrofsup  24114  cnvordtrestixx  24299  issgon  24494  ballotlem2  24734  mulsuble0b  25181  fprodcom2  25297  fprodcom  25298  coep  25363  dfpo2  25367  dfdm5  25387  dfrn5  25388  wfi  25462  frind  25498  tfrALTlem  25531  nocvxmin  25600  brtxp  25675  sscoid  25708  brimg  25732  funpartfun  25738  dfrdg4  25745  tfrqfree  25746  cgrcomlr  25880  ofscom  25889  btwnexch  25907  fscgr  25962  heibor1  26456  isdrngo3  26512  isdmn3  26621  an43OLD  26633  prtlem70  26635  prtlem90  26643  fz1eqin  26764  diophrex  26771  fphpd  26814  fzneg  26984  expdioph  27031  dford4  27037  lnr2i  27235  gsumcom3  27369  fgraphopab  27444  2reu3  27880  2reu7  27883  2reu8  27884  ndmaovcom  27983  f13dfv  28012  shwrdidx  28130  usgra2pth0  28186  usg2spthonot0  28230  frg2wot1  28304  frg2woteqm  28306  usg2spot2nb  28312  usgreg2spot  28314  uunT1p1  28747  uun132p1  28752  un2122  28756  uun2131p1  28758  uunT12p1  28766  uunT12p2  28767  uunT12p3  28768  uun2221  28779  uun2221p1  28780  uun2221p2  28781  3impdirp1  28782  ancomsimpVD  28831  bnj257  28925  bnj545  29120  bnj594  29137  lrelat  29651  islshpat  29654  atlrelat1  29958  ishlat2  29990  pmapglb  30406  polval2N  30542  cdlemb3  31242  diblsmopel  31808  dicelval3  31817  diclspsn  31831
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 178  df-an 361
  Copyright terms: Public domain W3C validator