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  1573  19.42  1816  eu1  2164  moaneu  2202  moanmo  2203  2eu3  2225  2eu6  2228  2eu7  2229  2eu8  2230  eq2tri  2342  r19.28av  2682  r19.29r  2684  r19.42v  2694  rexcomf  2699  rabswap  2719  euxfr2  2950  rmo4  2958  reu8  2961  rmo3  3078  incom  3361  difin2  3430  difin0ss  3520  ssunsn  3774  inuni  4173  eqvinop  4251  dfid3  4310  uniuni  4527  reuxfr2d  4557  elvvv  4749  brinxp2  4751  dmuni  4888  dfres2  5002  dfima2  5014  imadmrn  5024  imai  5027  asymref2  5060  cnvxp  5097  cnvcnvsn  5150  opswap  5159  mptpreima  5166  rnco  5179  ressn  5211  fncnv  5314  fununi  5316  fnres  5360  fnopabg  5367  dff1o2  5477  eqfnfv3  5624  respreima  5654  fsn  5696  fliftcnv  5810  isoini  5835  ndmovcom  6007  brtpos2  6240  brtpos  6243  tpostpos  6254  tposmpt2  6271  tfrlem7  6399  oaord  6545  oeeu  6601  nnaord  6617  pmex  6777  elpmg  6786  mapval2  6797  mapsnen  6938  map1  6939  xpsnen  6946  xpcomco  6952  elfi2  7168  supmo  7203  cp  7561  dfac5lem1  7750  dfac5lem2  7751  dfac5lem3  7752  dfac2  7757  kmlem3  7778  cdacomen  7807  cf0  7877  cflim3  7888  brdom7disj  8156  brdom6disj  8157  recmulnq  8588  letri3  8907  lesub0  9290  wloglei  9305  creur  9740  indstr  10287  xrltlen  10480  xrletri3  10486  qbtwnre  10526  xmulcom  10586  xmulneg1  10589  xmulf  10592  iooneg  10756  iccneg  10757  elfzuzb  10792  fzrev  10846  fzm1  10862  rediv  11616  imdiv  11623  lenegsq  11804  o1lo1  12011  fsumcom2  12237  fsumcom  12238  divalglem10  12601  smueqlem  12681  gcdcom  12699  isprm2  12766  infpn2  12960  imasleval  13443  invsym  13664  subsubc  13727  isffth2  13790  odulatb  14247  oduclatb  14248  resscntz  14807  oppgid  14829  gsumcom  15228  dfrhm2  15498  lsslss  15718  fiidomfld  16049  opsrtoslem1  16225  xrsdsreclb  16418  znleval  16508  istps3OLD  16660  ntreq0  16814  restopn2  16908  ist0-3  17073  1stcelcls  17187  txkgen  17346  trfil2  17582  elflim2  17659  flimrest  17678  txflf  17701  fclsrest  17719  tsmssubm  17825  ismet2  17898  blres  17977  metrest  18070  xrtgioo  18312  elii1  18433  evthicc2  18820  ovolfcl  18826  ovoliunlem1  18861  dyaddisj  18951  mbfaddlem  19015  itg1climres  19069  mbfi1fseqlem4  19073  iblpos  19147  itgposval  19150  ditgsplit  19211  ellimc3  19229  itgsubst  19396  deg1ldg  19478  sincosq1sgn  19866  sincosq3sgn  19868  cos11  19895  dvdsflsumcom  20428  fsumvma  20452  logfaclbnd  20461  dchrelbas3  20477  lgsdi  20571  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  h2hcau  21559  h2hlm  21560  axhcompl-zf  21578  nmopub  22488  nmfnleub  22505  chrelati  22944  cvexchlem  22948  mdsymlem8  22990  sumdmdii  22995  ballotlem2  23047  reuxfr3d  23138  iuninc  23158  rmo3f  23178  rmo4fOLD  23179  mptfnf  23226  xrofsup  23255  cnvordtrestixx  23297  xrsinvgval  23306  xrsmulgzz  23307  issgon  23484  isibfm  23593  eupath2lem2  23902  mulsuble0b  24088  coep  24108  dfpo2  24112  dfdm5  24132  dfrn5  24133  wfi  24207  frind  24243  tfrALTlem  24276  nocvxmin  24345  brtxp  24420  dffun10  24453  brimg  24476  brcup  24478  brcap  24479  funpartfun  24481  dfrdg4  24488  tfrqfree  24489  cgrcomlr  24621  ofscom  24630  btwnexch  24648  fscgr  24703  eeeeanv  24944  eqvinopb  24965  dff1o6f  25092  cmpdom  25143  dualded  25783  dualcat2  25784  lineval4a  26087  heibor1  26534  isdrngo3  26590  isdmn3  26699  an43OLD  26713  prtlem70  26715  prtlem90  26723  fz1eqin  26848  diophrex  26855  fphpd  26899  fzneg  27069  expdioph  27116  dford4  27122  lnr2i  27320  gsumcom3  27454  fgraphopab  27529  2reu3  27966  2reu7  27969  2reu8  27970  ndmaovcom  28065  uunT1p1  28556  uun132p1  28561  un2122  28565  uun2131p1  28567  uunT12p1  28575  uunT12p2  28576  uunT12p3  28577  uun2221  28588  uun2221p1  28589  uun2221p2  28590  3impdirp1  28591  ancomsimpVD  28641  bnj257  28732  bnj545  28927  bnj594  28944  lrelat  29204  islshpat  29207  atlrelat1  29511  ishlat2  29543  pmapglb  29959  polval2N  30095  cdlemb3  30795  diblsmopel  31361  dicelval3  31370  diclspsn  31384
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