Theorem ancom 460

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

Syntax hints:   ↔ wb 205   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  ancomd  461  biancomi  462  biancomd  463  ancomst  464  pm4.71r  558  pm5.32ri  575  pm5.32rd  577  bianassc  639  an12  641  an13  643  an42  653  andir  1005  cases2  1044  dfifp6  1065  ifpn  1070  excxor  1509  cador  1611  cadcoma  1615  exancom  1865  19.42v  1958  19.42  2232  sbel2x  2474  eu6  2574  moanmo  2624  2eu3  2655  2eu7  2659  2eu8  2660  eq2tri  2806  r19.42v  3276  rexcomf  3283  rabswap  3413  spc2ed  3530  euxfr2w  3650  euxfr2  3652  rmo4  3660  reu8  3663  rmo3f  3664  reuxfrd  3678  rmo3  3818  incomOLD  4132  difin2  4222  rcompleq  4226  euelss  4252  ssunsn  4758  uniprg  4853  inuni  5262  eqvinop  5395  elxp2  5604  elvvv  5653  brinxp2  5655  dmuni  5812  imadmrn  5968  asymref2  6011  cnvxp  6049  xpdifid  6060  cnvcnvsn  6111  opswap  6121  mptpreima  6130  xpco  6181  dfpo2  6188  fncnv  6491  fnres  6543  mptfnf  6552  dff1o2  6705  f13dfv  7127  fliftcnv  7162  isoini  7189  elrnmpores  7389  ndmovcom  7437  uniuni  7590  opabex3rd  7782  mptmpoopabbrd  7894  fsplit  7928  brtpos  8022  tposmpo  8050  oaord  8340  nnaord  8412  pmex  8578  mapsnend  8780  snmapen  8782  xpsnen  8796  xpcomco  8802  elfi2  9103  supmo  9141  infmo  9184  frind  9439  cp  9580  dfac5lem1  9810  dfac5lem2  9811  dfac2b  9817  kmlem3  9839  cflim3  9949  brdom7disj  10218  brdom6disj  10219  recmulnq  10651  lesub0  11422  wloglei  11437  creur  11897  indstr  12585  xmulcom  12929  xmulneg1  12932  xmulf  12935  iccneg  13133  fzrev  13248  injresinj  13436  rediv  14770  imdiv  14777  lenegsq  14960  o1lo1  15174  fsumcom2  15414  fsumcom  15415  fprodcom2  15622  fprodcom  15623  divalglem10  16039  smueqlem  16125  gcdcom  16148  lcmcom  16226  isprm2  16315  isprm7  16341  infpn2  16542  imasleval  17169  dfiso3  17402  posglbmo  18045  odulatb  18067  oduclatb  18140  oppgid  18878  gsumcom  19493  gsumcom3  19494  dfrhm2  19876  xrsdsreclb  20557  opsrtoslem1  21172  madutpos  21699  fvmptnn04if  21906  ntreq0  22136  ist0-3  22404  txkgen  22711  trfil2  22946  flimrest  23042  blres  23492  metrest  23586  restmetu  23632  elii1  24004  isclmp  24166  evthicc2  24529  ovolfcl  24535  dyaddisj  24665  iblpos  24862  itgposval  24865  ditgsplit  24930  itgsubst  25118  sincosq3sgn  25562  cos11  25594  dvdsflsumcom  26242  fsumvma  26266  logfaclbnd  26275  dchrelbas3  26291  lgsdi  26387  lgsquadlem3  26435  2lgslem1a  26444  istrkg2ld  26725  tgjustf  26738  tgcgr4  26796  mirreu3  26919  hpgcom  27032  colhp  27035  dfcgra2  27095  nbgrel  27610  nbgrsym  27633  wlkson  27926  isspthonpth  28018  usgr2pth0  28034  wwlksnextinj  28165  elwspths2spth  28233  rusgrnumwwlkl1  28234  clwwlknclwwlkdifnum  28245  clwwlkn1  28306  clwwlkn2  28309  iseupthf1o  28467  eupth2lem2  28484  frgrncvvdeqlem2  28565  fusgr2wsp2nb  28599  fusgreg2wsp  28601  frgrreg  28659  frgrregord013  28660  h2hcau  29242  nmopub  30171  nmfnleub  30188  chrelati  30627  cvexchlem  30631  mdsymlem8  30673  sumdmdii  30678  nelbOLDOLD  30718  2reucom  30729  reuxfrdf  30740  dmrab  30745  difrab2  30746  ressupprn  30926  2ndpreima  30942  fpwrelmapffslem  30969  xrofsup  30992  mgccnv  31179  pmtrprfv2  31259  smatrcl  31648  cnvordtrestixx  31765  issgon  31991  eulerpartlemr  32241  eulerpartlemgvv  32243  ballotlem2  32355  sgn3da  32408  oddprm2  32535  bnj257  32586  bnj545  32775  bnj594  32792  satfv0  33220  satfvsuclem1  33221  dfdm5  33653  dfrn5  33654  elima4  33656  sletri3  33885  nocvxmin  33900  sltrec  33941  elfix  34132  dffix2  34134  brimg  34166  brsuccf  34170  dfrecs2  34179  dfrdg4  34180  cgrcomlr  34227  ofscom  34236  btwnexch  34254  fscgr  34309  bj-df-ifc  34688  bj-dfmpoa  35216  bj-eldiag  35274  bj-imdirco  35288  bj-ccinftydisj  35311  mptsnunlem  35436  topdifinffinlem  35445  fvineqsneq  35510  wl-cases2-dnf  35598  wl-ax11-lem4  35666  fin2solem  35690  poimirlem26  35730  poimirlem30  35734  poimirlem32  35736  ftc1anclem6  35782  ftc1anc  35785  heibor1  35895  isdrngo3  36044  isdmn3  36159  an2anr  36305  anan  36306  inxpxrn  36448  prtlem70  36798  lrelat  36955  islshpat  36958  atlrelat1  37262  ishlat2  37294  cdlemb3  38547  diblsmopel  39112  dicelval3  39121  diclspsn  39135  uzindd  39913  3factsumint2  39958  3factsumint3  39959  3factsumint  39961  fz1eqin  40507  diophrex  40513  fphpd  40554  fzneg  40720  expdioph  40761  dford4  40767  lnr2i  40857  fgraphopab  40951  ifpancor  40969  ifpidg  40996  ifpid2g  40998  ifpid1g  40999  ifpim23g  41000  rp-fakeoranass  41019  dfid7  41109  dfrtrcl5  41126  relexp0eq  41198  fsovrfovd  41506  rr-grothprimbi  41802  uunT1p1  42290  uun132p1  42295  un2122  42299  uun2131p1  42301  uunT12p1  42309  uunT12p2  42310  uunT12p3  42311  uun2221  42322  uun2221p1  42323  uun2221p2  42324  3impdirp1  42325  ancomstVD  42374  icccncfext  43318  dvnmul  43374  dvmptfprodlem  43375  dvnprodlem2  43378  fourierdlem42  43580  fourierdlem83  43620  f1cof1b  44456  2reu3  44489  2reu7  44490  2reu8  44491  2reuimp0  44493  ndmaovcom  44584  an4com24  44647  4an21  44649  sprvalpwn0  44823  prpair  44841  prproropf1olem0  44842  2zrngnmrid  45396  opeliun2xp  45556  rrx2linest  45976  pm5.32dav  46027  iscnrm3lem3  46117  thincsect2  46227