Theorem ancom 463

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ancomd  464  biancomi  465  biancomd  466  ancomst  467  pm4.71r  561  pm5.32ri  578  pm5.32rd  580  bianassc  641  an12  643  an13  645  an42  655  andir  1005  cases2  1042  dfifp6  1063  excxor  1507  cador  1609  cadcoma  1613  exancom  1861  19.42v  1954  19.42  2238  sbel2x  2498  eu6  2659  moanmo  2707  2eu3  2738  2eu7  2743  2eu8  2744  eq2tri  2883  r19.28vOLD  3187  r19.29rOLD  3256  r19.42v  3350  rexcomOLD  3356  rexcomf  3358  rabswap  3488  spc2ed  3602  euxfr2w  3711  euxfr2  3713  rmo4  3721  reu8  3724  rmo3f  3725  reuxfrd  3739  rmo3  3872  rmo3OLD  3873  incomOLD  4179  difin2  4266  euelss  4290  ssunsn  4761  inuni  5246  eqvinop  5378  elxp2  5579  elvvv  5627  brinxp2  5629  dmuni  5783  imadmrn  5939  asymref2  5977  cnvxp  6014  xpdifid  6025  cnvcnvsn  6076  opswap  6086  mptpreima  6092  xpco  6140  fncnv  6427  fnres  6474  mptfnf  6483  dff1o2  6620  f13dfv  7031  fliftcnv  7064  isoini  7091  elrnmpores  7288  ndmovcom  7335  uniuni  7484  opabex3rd  7667  mptmpoopabbrd  7778  fsplit  7812  brtpos  7901  tposmpo  7929  oaord  8173  nnaord  8245  pmex  8411  mapsnend  8588  snmapen  8590  xpsnen  8601  xpcomco  8607  elfi2  8878  supmo  8916  infmo  8959  cp  9320  dfac5lem1  9549  dfac5lem2  9550  dfac2b  9556  kmlem3  9578  cflim3  9684  brdom7disj  9953  brdom6disj  9954  recmulnq  10386  lesub0  11157  wloglei  11172  creur  11632  indstr  12317  xmulcom  12660  xmulneg1  12663  xmulf  12666  iccneg  12859  fzrev  12971  injresinj  13159  rediv  14490  imdiv  14497  lenegsq  14680  o1lo1  14894  fsumcom2  15129  fsumcom  15130  fprodcom2  15338  fprodcom  15339  divalglem10  15753  smueqlem  15839  gcdcom  15862  lcmcom  15937  isprm2  16026  isprm7  16052  infpn2  16249  imasleval  16814  dfiso3  17043  odulatb  17753  oduclatb  17754  posglbmo  17757  oppgid  18484  gsumcom  19097  gsumcom3  19098  dfrhm2  19469  opsrtoslem1  20264  xrsdsreclb  20592  madutpos  21251  fvmptnn04if  21457  ntreq0  21685  ist0-3  21953  txkgen  22260  trfil2  22495  flimrest  22591  blres  23041  metrest  23134  restmetu  23180  elii1  23539  isclmp  23701  evthicc2  24061  ovolfcl  24067  dyaddisj  24197  iblpos  24393  itgposval  24396  ditgsplit  24459  itgsubst  24646  sincosq3sgn  25086  cos11  25117  dvdsflsumcom  25765  fsumvma  25789  logfaclbnd  25798  dchrelbas3  25814  lgsdi  25910  lgsquadlem3  25958  2lgslem1a  25967  istrkg2ld  26246  tgjustf  26259  tgcgr4  26317  mirreu3  26440  hpgcom  26553  colhp  26556  dfcgra2  26616  nbgrel  27122  nbgrsym  27145  wlkson  27438  isspthonpth  27530  usgr2pth0  27546  wwlksnextinj  27677  elwspths2spth  27746  rusgrnumwwlkl1  27747  clwwlknclwwlkdifnum  27758  clwwlkn1  27819  clwwlkn2  27822  iseupthf1o  27981  eupth2lem2  27998  frgrncvvdeqlem2  28079  fusgr2wsp2nb  28113  fusgreg2wsp  28115  frgrreg  28173  frgrregord013  28174  h2hcau  28756  nmopub  29685  nmfnleub  29702  chrelati  30141  cvexchlem  30145  mdsymlem8  30187  sumdmdii  30192  nelbOLD  30232  2reucom  30243  reuxfrdf  30255  dmrab  30260  difrab2  30261  2ndpreima  30443  fpwrelmapffslem  30468  xrofsup  30492  pmtrprfv2  30732  smatrcl  31061  cnvordtrestixx  31156  issgon  31382  eulerpartlemr  31632  eulerpartlemgvv  31634  ballotlem2  31746  sgn3da  31799  oddprm2  31926  bnj257  31977  bnj545  32167  bnj594  32184  satfv0  32605  satfvsuclem1  32606  dfpo2  32991  dfdm5  33016  dfrn5  33017  elima4  33019  frind  33085  sletri3  33234  nocvxmin  33248  sltrec  33278  elfix  33364  dffix2  33366  brimg  33398  brsuccf  33402  dfrecs2  33411  dfrdg4  33412  cgrcomlr  33459  ofscom  33468  btwnexch  33486  fscgr  33541  bj-df-ifc  33913  bj-dfmpoa  34413  bj-eldiag  34471  bj-ccinftydisj  34498  mptsnunlem  34622  topdifinffinlem  34631  fvineqsneq  34696  wl-cases2-dnf  34767  wl-ax11-lem4  34835  fin2solem  34893  poimirlem4  34911  poimirlem26  34933  poimirlem30  34937  poimirlem32  34939  ftc1anclem6  34987  ftc1anc  34990  heibor1  35103  isdrngo3  35252  isdmn3  35367  an2anr  35513  anan  35514  inxpxrn  35658  prtlem70  36008  lrelat  36165  islshpat  36168  atlrelat1  36472  ishlat2  36504  cdlemb3  37757  diblsmopel  38322  dicelval3  38331  diclspsn  38345  fz1eqin  39386  diophrex  39392  fphpd  39433  fzneg  39599  expdioph  39640  dford4  39646  lnr2i  39736  fgraphopab  39830  ifpancor  39849  ifpdfbi  39859  ifpidg  39877  ifpid2g  39879  ifpid1g  39880  ifpim23g  39881  rp-fakeoranass  39900  dfid7  39992  dfrtrcl5  40009  relexp0eq  40066  fsovrfovd  40375  rcompleq  40390  rr-grothprimbi  40651  uunT1p1  41135  uun132p1  41140  un2122  41144  uun2131p1  41146  uunT12p1  41154  uunT12p2  41155  uunT12p3  41156  uun2221  41167  uun2221p1  41168  uun2221p2  41169  3impdirp1  41170  ancomstVD  41219  icccncfext  42190  dvnmul  42248  dvmptfprodlem  42249  dvnprodlem2  42252  fourierdlem42  42454  fourierdlem83  42494  2reu3  43329  2reu7  43330  2reu8  43331  2reuimp0  43333  ndmaovcom  43424  an4com24  43487  4an21  43489  sprvalpwn0  43665  prpair  43683  prproropf1olem0  43684  2zrngnmrid  44241  opeliun2xp  44401  rrx2linest  44749