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

Step	Hyp	Ref	Expression
1		pm3.22 437	. 2 |- ( ( ph /\ ps ) -> ( ps /\ ph ) )
2		pm3.22 437	. 2 |- ( ( ps /\ ph ) -> ( ph /\ ps ) )
3	1, 2	impbii 181	1 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )

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  1296  excxor  1315  ancomsimp  1375  cador  1397  cadcoma  1401  cadcomb  1402  cad1  1404  exancom  1593  19.42  1898  eu1  2275  moaneu  2313  moanmo  2314  2eu3  2336  2eu6  2339  2eu7  2340  2eu8  2341  eq2tri  2463  r19.28av  2805  r19.29r  2807  r19.42v  2822  rexcomf  2827  rabswap  2847  euxfr2  3079  rmo4  3087  reu8  3090  rmo3  3208  incom  3493  difin2  3563  difin0ss  3654  ssunsn  3919  inuni  4322  eqvinop  4401  dfid3  4459  uniuni  4675  reuxfr2d  4705  elvvv  4896  brinxp2  4898  dmuni  5038  dfres2  5152  dfima2  5164  imadmrn  5174  imai  5177  asymref2  5210  cnvxp  5249  cnvcnvsn  5306  opswap  5315  mptpreima  5322  rnco  5335  ressn  5367  xpco  5373  fncnv  5474  fununi  5476  fnres  5520  fnopabg  5527  dff1o2  5638  eqfnfv3  5788  respreima  5818  fsn  5865  fliftcnv  5992  isoini  6017  ndmovcom  6193  brtpos2  6444  brtpos  6447  tpostpos  6458  tposmpt2  6475  tfrlem7  6603  oaord  6749  oeeu  6805  nnaord  6821  pmex  6982  elpmg  6991  mapval2  7002  mapsnen  7143  map1  7144  xpsnen  7151  xpcomco  7157  elfi2  7377  supmo  7413  cp  7771  dfac5lem1  7960  dfac5lem2  7961  dfac5lem3  7962  dfac2  7967  kmlem3  7988  cdacomen  8017  cf0  8087  cflim3  8098  brdom7disj  8365  brdom6disj  8366  recmulnq  8797  letri3  9116  lesub0  9500  wloglei  9515  creur  9950  indstr  10501  xrltlen  10695  xrletri3  10701  qbtwnre  10741  xmulcom  10801  xmulneg1  10804  xmulf  10807  iooneg  10973  iccneg  10974  elfzuzb  11009  fzrev  11064  fzm1  11082  injresinj  11155  rediv  11891  imdiv  11898  lenegsq  12079  o1lo1  12286  fsumcom2  12513  fsumcom  12514  divalglem10  12877  smueqlem  12957  gcdcom  12975  isprm2  13042  infpn2  13236  imasleval  13721  invsym  13942  subsubc  14005  isffth2  14068  odulatb  14525  oduclatb  14526  resscntz  15085  oppgid  15107  gsumcom  15506  dfrhm2  15776  lsslss  15992  fiidomfld  16323  opsrtoslem1  16499  xrsdsreclb  16700  znleval  16790  istps3OLD  16942  ntreq0  17096  restopn2  17195  ist0-3  17363  1stcelcls  17477  txkgen  17637  trfil2  17872  elflim2  17949  flimrest  17968  txflf  17991  fclsrest  18009  tsmssubm  18125  ismet2  18316  blres  18414  metrest  18507  restmetu  18570  xrtgioo  18790  elii1  18913  evthicc2  19310  ovolfcl  19316  ovoliunlem1  19351  dyaddisj  19441  mbfaddlem  19505  itg1climres  19559  mbfi1fseqlem4  19563  iblpos  19637  itgposval  19640  ditgsplit  19701  ellimc3  19719  itgsubst  19886  deg1ldg  19968  sincosq1sgn  20359  sincosq3sgn  20361  cos11  20388  dvdsflsumcom  20926  fsumvma  20950  logfaclbnd  20959  dchrelbas3  20975  lgsdi  21069  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  cusgra3v  21426  trls  21489  trlon  21493  pthon  21528  spthon  21535  3v3e3cycl2  21604  eupath2lem2  21653  h2hcau  22435  h2hlm  22436  axhcompl-zf  22454  nmopub  23364  nmfnleub  23381  chrelati  23820  cvexchlem  23824  mdsymlem8  23866  sumdmdii  23871  reuxfr3d  23929  rmo3f  23935  rmo4fOLD  23936  mptfnf  24026  2ndpreima  24049  xrofsup  24079  cnvordtrestixx  24264  issgon  24459  ballotlem2  24699  mulsuble0b  25146  fprodcom2  25261  fprodcom  25262  coep  25322  dfpo2  25326  dfdm5  25346  dfrn5  25347  wfi  25421  frind  25457  tfrALTlem  25490  nocvxmin  25559  brtxp  25634  dffun10  25667  brimg  25690  brcup  25692  brcap  25693  funpartfun  25696  dfrdg4  25703  tfrqfree  25704  cgrcomlr  25836  ofscom  25845  btwnexch  25863  fscgr  25918  heibor1  26409  isdrngo3  26465  isdmn3  26574  an43OLD  26586  prtlem70  26588  prtlem90  26596  fz1eqin  26717  diophrex  26724  fphpd  26767  fzneg  26937  expdioph  26984  dford4  26990  lnr2i  27188  gsumcom3  27322  fgraphopab  27397  2reu3  27833  2reu7  27836  2reu8  27837  ndmaovcom  27936  f13dfv  27962  usgra2pth0  28042  usg2spthonot0  28086  frg2wot1  28160  frg2woteqm  28162  usg2spot2nb  28168  usgreg2spot  28170  uunT1p1  28602  uun132p1  28607  un2122  28611  uun2131p1  28613  uunT12p1  28621  uunT12p2  28622  uunT12p3  28623  uun2221  28634  uun2221p1  28635  uun2221p2  28636  3impdirp1  28637  ancomsimpVD  28686  bnj257  28777  bnj545  28972  bnj594  28989  lrelat  29497  islshpat  29500  atlrelat1  29804  ishlat2  29836  pmapglb  30252  polval2N  30388  cdlemb3  31088  diblsmopel  31654  dicelval3  31663  diclspsn  31677

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