Theorem ancom 450

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	⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

Proof of Theorem ancom

Step	Hyp	Ref	Expression
1		pm3.22 449	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))
2		pm3.22 449	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓))
3	1, 2	impbii 200	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 197   ∧ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 198  df-an 385

This theorem is referenced by:  ancomd  451  ancomst  452  ancomsd  453  pm4.71r  550  pm5.32ri  567  pm5.32rd  569  anbi2ci  613  anbi12ci  615  an21  626  an32  628  an13  629  an42  639  andir  1022  cases2  1061  dfbi3OLD  1064  dfifp6  1084  3ancomaOLD  1113  3anrotOLD  1117  nancom  1604  excxor  1623  cador  1702  cadcoma  1706  exancom  1947  19.42v  2043  19.42  2272  sbel2x  2618  moanmo  2693  2eu3  2716  2eu7  2720  2eu8  2721  eq2tri  2863  r19.28v  3255  r19.29r  3257  r19.42v  3276  rexcomf  3281  rabswap  3306  euxfr2  3583  rmo4  3591  reu8  3594  rmo3  3717  incom  3998  difin2  4085  euelss  4109  ssunsn  4543  inuni  5012  reuxfr2d  5082  eqvinop  5138  dfid3  5214  elxp2  5328  elvvv  5372  brinxp2  5374  brinxp2OLD  5375  dmuni  5529  dfres2  5652  restidsing  5664  dfima2  5672  imadmrn  5680  imai  5682  asymref2  5718  cnvxp  5756  xpdifid  5767  cnvcnvsn  5818  opswap  5830  mptpreima  5836  rnco  5849  ressn  5879  xpco  5883  wfi  5920  elon2  5941  fncnv  6167  fununi  6169  fnres  6212  mptfnf  6220  fnopabg  6222  dff1o2  6352  eqfnfv3  6529  respreima  6560  fsn  6619  f13dfv  6748  fliftcnv  6779  isoini  6806  elrnmpt2res  6998  ndmovcom  7045  uniuni  7195  mptmpt2opabbrd  7475  brtpos2  7587  brtpos  7590  tpostpos  7601  tposmpt2  7618  mpt2curryd  7624  oaord  7858  oeeu  7914  nnaord  7930  pmex  8091  elpmg  8102  mapval2  8116  mapsnend  8265  snmapen  8267  xpsnen  8277  xpcomco  8283  elfi2  8553  supmo  8591  infmo  8634  cp  8995  dfac5lem1  9223  dfac5lem2  9224  dfac5lem3  9225  dfac2b  9230  dfac2OLD  9232  kmlem3  9253  cdacomen  9282  cf0  9352  cflim3  9363  brdom7disj  9632  brdom6disj  9633  recmulnq  10065  letri3  10402  lesub0  10824  wloglei  10839  mulsuble0b  11174  creur  11293  indstr  11969  xrltlen  12189  xrletri3  12197  qbtwnre  12242  xmulcom  12308  xmulneg1  12311  xmulf  12314  iooneg  12507  iccneg  12508  elfzuzb  12553  fzrev  12620  ssfzoulel  12780  injresinj  12807  xpcogend  13932  rediv  14088  imdiv  14095  lenegsq  14277  o1lo1  14485  fsumcom2  14722  fsumcom  14723  fprodcom2  14929  fprodcom  14930  divalglem10  15339  smueqlem  15425  gcdcom  15448  dfgcd2  15476  lcmcom  15519  isprm2  15607  isprm7  15631  infpn2  15828  imasleval  16400  invsym  16620  dfiso3  16631  subsubc  16711  isffth2  16774  odulatb  17342  oduclatb  17343  posglbmo  17346  resscntz  17959  oppgid  17981  gsumcom  18571  dfrhm2  18915  lsslss  19162  fiidomfld  19511  opsrtoslem1  19686  xrsdsreclb  19995  znleval  20104  gsumcom3  20409  madutpos  20653  fvmptnn04if  20861  ntreq0  21089  restopn2  21189  ist0-3  21357  1stcelcls  21472  txkgen  21663  trfil2  21898  elflim2  21975  flimrest  21994  txflf  22017  fclsrest  22035  tsmssubm  22153  ismet2  22345  blres  22443  metrest  22536  restmetu  22582  xrtgioo  22816  elii1  22941  isclmp  23103  isncvsngp  23155  evthicc2  23435  ovolfcl  23441  ovoliunlem1  23477  dyaddisj  23571  mbfaddlem  23635  itg1climres  23689  mbfi1fseqlem4  23693  iblpos  23767  itgposval  23770  ditgsplit  23833  ellimc3  23851  itgsubst  24020  deg1ldg  24060  sincosq1sgn  24459  sincosq3sgn  24461  cos11  24488  dvdsflsumcom  25122  fsumvma  25146  logfaclbnd  25155  dchrelbas3  25171  lgsdi  25267  lgsquadlem1  25313  lgsquadlem2  25314  lgsquadlem3  25315  2lgslem1a  25324  istrkg2ld  25567  tgcgr4  25634  mirreu3  25757  hpgcom  25867  colhp  25870  dfcgra2  25929  nbgrel  26443  nbgrelOLD  26444  nbgrsym  26473  nbgrsymOLD  26474  wlkson  26774  isspthonpth  26867  usgr2pth0  26883  wwlksnextinj  27030  elwspths2spth  27103  rusgrnumwwlkl1  27104  clwwlknclwwlkdifnum  27115  clwwlkn1  27184  clwwlkn2  27187  0clwlk  27297  iseupthf1o  27369  eupth2lem2  27386  frgrncvvdeqlem2  27469  fusgr2wsp2nb  27503  fusgreg2wsp  27505  numclwwlkqhash  27549  frgrreg  27576  frgrregord013  27577  h2hcau  28158  h2hlm  28159  axhcompl-zf  28177  nmopub  29089  nmfnleub  29106  chrelati  29545  cvexchlem  29549  mdsymlem8  29591  sumdmdii  29596  spc2ed  29634  reuxfr3d  29649  rmo3f  29655  rmo4fOLD  29656  difrab2  29658  2ndpreima  29806  fpwrelmapffslem  29828  xrofsup  29854  pmtrprfv2  30167  smatrcl  30181  cnvordtrestixx  30278  issgon  30505  eulerpartlemr  30755  eulerpartlemgvv  30757  ballotlem2  30869  sgn3da  30922  oddprm2  31052  bnj257  31092  bnj545  31282  bnj594  31299  coep  31957  dfpo2  31961  dfdm5  31990  dfrn5  31991  elima4  31993  frpoind  32055  frind  32058  sletri3  32195  nocvxmin  32209  sltrec  32239  brtxp  32302  elfix  32325  dffix2  32327  sscoid  32335  brimg  32359  brsuccf  32363  funpartfun  32365  dfrecs2  32372  dfrdg4  32373  cgrcomlr  32420  ofscom  32429  btwnexch  32447  fscgr  32502  bj-dfifc2  32873  bj-restuni  33355  bj-0int  33360  bj-dfmpt2a  33376  bj-eldiag  33402  bj-ccinftydisj  33411  mptsnunlem  33496  topdifinffinlem  33505  wl-cases2-dnf  33605  wl-ax11-lem4  33673  fin2solem  33702  poimirlem4  33720  poimirlem26  33742  poimirlem30  33746  poimirlem32  33748  ftc1anclem6  33796  ftc1anc  33799  heibor1  33914  isdrngo3  34063  isdmn3  34178  biancom  34309  biancomd  34310  an2anr  34313  anan  34314  inxpxrn  34460  prtlem70  34629  lrelat  34788  islshpat  34791  atlrelat1  35095  ishlat2  35127  pmapglb  35544  polval2N  35680  cdlemb3  36381  diblsmopel  36946  dicelval3  36955  diclspsn  36969  fz1eqin  37828  diophrex  37835  fphpd  37876  fzneg  38044  expdioph  38085  dford4  38091  lnr2i  38181  fgraphopab  38283  ifpancor  38302  ifpdfbi  38312  ifpidg  38330  ifpid2g  38332  ifpid1g  38333  ifpim23g  38334  ifp1bi  38341  rp-fakeoranass  38353  dfid7  38413  dfrtrcl5  38430  relexp0eq  38487  fsovrfovd  38797  rcompleq  38812  uunT1p1  39499  uun132p1  39504  un2122  39508  uun2131p1  39510  uunT12p1  39518  uunT12p2  39519  uunT12p3  39520  uun2221  39531  uun2221p1  39532  uun2221p2  39533  3impdirp1  39534  ancomstVD  39589  icccncfext  40574  dvnmul  40632  dvmptfprodlem  40633  dvnprodlem2  40636  fourierdlem42  40839  fourierdlem83  40879  2reu3  41694  2reu7  41697  2reu8  41698  ndmaovcom  41788  an4com24  41851  4an21  41853  sprvalpwn0  42295  2zrngnmrid  42512  opeliun2xp  42673  eliunxp2  42674