Theorem ancom 466

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 465	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))
2		pm3.22 465	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓))
3	1, 2	impbii 199	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 196   ∧ 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 197  df-an 386

This theorem is referenced by:  ancomd  467  ancomst  468  ancomsd  470  pm4.71r  663  pm5.32ri  670  pm5.32rd  672  anbi2ci  732  anbi12ci  734  an12  838  an32  839  an13  840  an42  866  andir  912  dfbi3OLD  995  dfifp6  1018  3anrot  1043  3ancoma  1045  nancom  1450  excxor  1469  cador  1547  cadcoma  1551  exancom  1787  19.42v  1918  19.42  2105  sbel2x  2459  moanmo  2532  2eu3  2555  2eu7  2559  2eu8  2560  eq2tri  2683  r19.28v  3071  r19.29r  3073  r19.42v  3092  rexcomf  3097  rabswap  3121  euxfr2  3391  rmo4  3399  reu8  3402  rmo3  3528  incom  3805  difin2  3890  euelss  3914  ssunsn  4360  inuni  4826  reuxfr2d  4891  eqvinop  4955  dfid3  5025  elxp2  5132  elvvv  5178  brinxp2  5180  dmuni  5334  dfres2  5453  restidsing  5458  dfima2  5468  imadmrn  5476  imai  5478  asymref2  5513  cnvxp  5551  xpdifid  5562  cnvcnvsn  5612  opswap  5622  mptpreima  5628  rnco  5641  ressn  5671  xpco  5675  wfi  5713  elon2  5734  fncnv  5962  fununi  5964  fnres  6007  mptfnf  6015  fnopabg  6017  dff1o2  6142  eqfnfv3  6313  respreima  6344  fsn  6402  f13dfv  6530  fliftcnv  6561  isoini  6588  elrnmpt2res  6774  ndmovcom  6821  uniuni  6971  mptmpt2opabbrd  7248  brtpos2  7358  brtpos  7361  tpostpos  7372  tposmpt2  7389  mpt2curryd  7395  oaord  7627  oeeu  7683  nnaord  7699  pmex  7862  elpmg  7873  mapval2  7887  mapsnen  8035  map1  8036  xpsnen  8044  xpcomco  8050  elfi2  8320  supmo  8358  infmo  8401  cp  8754  dfac5lem1  8946  dfac5lem2  8947  dfac5lem3  8948  dfac2  8953  kmlem3  8974  cdacomen  9003  cf0  9073  cflim3  9084  brdom7disj  9353  brdom6disj  9354  recmulnq  9786  letri3  10123  lesub0  10545  wloglei  10560  mulsuble0b  10895  creur  11014  indstr  11756  xrltlen  11979  xrletri3  11985  qbtwnre  12030  xmulcom  12096  xmulneg1  12099  xmulf  12102  iooneg  12292  iccneg  12293  elfzuzb  12336  fzrev  12403  ssfzoulel  12562  injresinj  12589  xpcogend  13713  rediv  13871  imdiv  13878  lenegsq  14060  o1lo1  14268  fsumcom2  14505  fsumcom2OLD  14506  fsumcom  14507  fprodcom2  14714  fprodcom2OLD  14715  fprodcom  14716  divalglem10  15125  smueqlem  15212  gcdcom  15235  dfgcd2  15263  lcmcom  15306  isprm2  15395  isprm7  15420  infpn2  15617  imasleval  16201  invsym  16422  dfiso3  16433  subsubc  16513  isffth2  16576  odulatb  17143  oduclatb  17144  posglbmo  17147  resscntz  17764  oppgid  17786  gsumcom  18376  dfrhm2  18717  lsslss  18961  fiidomfld  19308  opsrtoslem1  19484  xrsdsreclb  19793  znleval  19903  gsumcom3  20205  madutpos  20448  fvmptnn04if  20654  ntreq0  20881  restopn2  20981  ist0-3  21149  1stcelcls  21264  txkgen  21455  trfil2  21691  elflim2  21768  flimrest  21787  txflf  21810  fclsrest  21828  tsmssubm  21946  ismet2  22138  blres  22236  metrest  22329  restmetu  22375  xrtgioo  22609  elii1  22734  isclmp  22897  isncvsngp  22949  evthicc2  23229  ovolfcl  23235  ovoliunlem1  23270  dyaddisj  23364  mbfaddlem  23427  itg1climres  23481  mbfi1fseqlem4  23485  iblpos  23559  itgposval  23562  ditgsplit  23625  ellimc3  23643  itgsubst  23812  deg1ldg  23852  sincosq1sgn  24250  sincosq3sgn  24252  cos11  24279  dvdsflsumcom  24914  fsumvma  24938  logfaclbnd  24947  dchrelbas3  24963  lgsdi  25059  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  2lgslem1a  25116  istrkg2ld  25359  tgcgr4  25426  mirreu3  25549  hpgcom  25659  colhp  25662  dfcgra2  25721  nbgrel  26238  nbgrsym  26265  wlkson  26552  isspthonpth  26645  usgr2pth0  26661  wwlksnextinj  26794  elwspths2spth  26862  rusgrnumwwlkl1  26863  clwwlksn2  26910  0clwlk  26991  iseupthf1o  27062  eupth2lem2  27079  frgrncvvdeqlem2  27164  fusgr2wsp2nb  27198  fusgreg2wsp  27200  numclwwlkovf2  27217  frgrreg  27252  frgrregord013  27253  h2hcau  27836  h2hlm  27837  axhcompl-zf  27855  nmopub  28767  nmfnleub  28784  chrelati  29223  cvexchlem  29227  mdsymlem8  29269  sumdmdii  29274  spc2ed  29312  reuxfr3d  29329  rmo3f  29335  rmo4fOLD  29336  difrab2  29339  2ndpreima  29485  fpwrelmapffslem  29507  xrofsup  29533  pmtrprfv2  29848  smatrcl  29862  cnvordtrestixx  29959  issgon  30186  eulerpartlemr  30436  eulerpartlemgvv  30438  ballotlem2  30550  sgn3da  30603  oddprm2  30733  bnj257  30773  bnj545  30965  bnj594  30982  coep  31641  dfpo2  31645  dfdm5  31676  dfrn5  31677  elima4  31679  frind  31740  sletri3  31880  nocvxmin  31894  sltrec  31924  brtxp  31987  elfix  32010  dffix2  32012  sscoid  32020  brimg  32044  brsuccf  32048  funpartfun  32050  dfrecs2  32057  dfrdg4  32058  cgrcomlr  32105  ofscom  32114  btwnexch  32132  fscgr  32187  bj-dfifc2  32564  bj-restuni  33050  bj-0int  33055  bj-dfmpt2a  33071  bj-eldiag  33091  bj-ccinftydisj  33100  mptsnunlem  33185  topdifinffinlem  33195  wl-cases2-dnf  33295  wl-ax11-lem4  33365  fin2solem  33395  poimirlem4  33413  poimirlem26  33435  poimirlem30  33439  poimirlem32  33441  ftc1anclem6  33490  ftc1anc  33493  heibor1  33609  isdrngo3  33758  isdmn3  33873  biancom  33994  biancomd  33995  an2anr  33998  anan  33999  brinxp2ALTV  34034  prtlem70  34141  lrelat  34301  islshpat  34304  atlrelat1  34608  ishlat2  34640  pmapglb  35056  polval2N  35192  cdlemb3  35894  diblsmopel  36460  dicelval3  36469  diclspsn  36483  fz1eqin  37332  diophrex  37339  fphpd  37380  fzneg  37549  expdioph  37590  dford4  37596  lnr2i  37686  fgraphopab  37788  ifpancor  37808  ifpdfbi  37818  ifpidg  37836  ifpid2g  37838  ifpid1g  37839  ifpim23g  37840  ifp1bi  37847  rp-fakeoranass  37859  dfid7  37919  dfrtrcl5  37936  relexp0eq  37993  fsovrfovd  38303  rcompleq  38318  uunT1p1  39008  uun132p1  39013  un2122  39017  uun2131p1  39019  uunT12p1  39027  uunT12p2  39028  uunT12p3  39029  uun2221  39040  uun2221p1  39041  uun2221p2  39042  3impdirp1  39043  ancomstVD  39101  mapsnend  39391  icccncfext  40100  dvnmul  40158  dvmptfprodlem  40159  dvnprodlem2  40162  fourierdlem42  40366  fourierdlem83  40406  2reu3  41188  2reu7  41191  2reu8  41192  ndmaovcom  41285  sprvalpwn0  41733  2zrngnmrid  41950  opeliun2xp  42111  eliunxp2  42112