Theorem ancom 454

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

Syntax hints:   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  ancomd  455  biancomi  456  biancomd  457  ancomst  458  ancomsd  459  pm4.71r  554  pm5.32ri  571  pm5.32rd  573  bianassc  633  an21  634  an32  636  an13  637  an42  647  andir  994  cases2  1031  dfifp6  1052  3ancomaOLD  1083  3anrotOLD  1087  nancomOLD  1563  excxor  1587  cador  1666  cadcoma  1670  exancom  1905  19.42v  1996  19.42  2223  sbel2x  2538  eu6OLD  2594  moanmo  2658  2eu3  2683  2eu3OLD  2684  2eu7  2688  2eu8  2689  eq2tri  2841  r19.28v  3257  r19.29r  3259  r19.42v  3278  rexcomf  3283  rabswap  3308  euxfr2  3603  rmo4  3611  reu8  3614  rmo3f  3615  reuxfr3d  3626  rmo3  3745  rmo3OLD  3746  incom  4028  difin2  4116  euelss  4140  ssunsn  4590  inuni  5060  eqvinop  5186  elxp2  5379  elvvv  5424  brinxp2  5426  brinxp2OLD  5427  dmuni  5579  imadmrn  5730  asymref2  5768  cnvxp  5805  xpdifid  5816  cnvcnvsn  5866  opswap  5876  mptpreima  5882  xpco  5929  fncnv  6207  fnres  6253  mptfnf  6261  dff1o2  6396  f13dfv  6802  fliftcnv  6833  isoini  6860  elrnmpt2res  7051  ndmovcom  7098  uniuni  7248  mptmpt2opabbrd  7528  brtpos  7643  tposmpt2  7671  oaord  7911  nnaord  7983  pmex  8145  mapsnend  8320  snmapen  8322  xpsnen  8332  xpcomco  8338  elfi2  8608  supmo  8646  infmo  8689  cp  9051  dfac5lem1  9279  dfac5lem2  9280  dfac2b  9286  dfac2OLD  9288  kmlem3  9309  cdacomen  9338  cflim3  9419  brdom7disj  9688  brdom6disj  9689  recmulnq  10121  lesub0  10892  wloglei  10907  creur  11368  indstr  12063  xmulcom  12408  xmulneg1  12411  xmulf  12414  iccneg  12608  fzrev  12721  injresinj  12908  rediv  14278  imdiv  14285  lenegsq  14467  o1lo1  14676  fsumcom2  14910  fsumcom  14911  fprodcom2  15117  fprodcom  15118  divalglem10  15532  smueqlem  15618  gcdcom  15641  lcmcom  15712  isprm2  15800  isprm7  15824  infpn2  16021  imasleval  16587  dfiso3  16818  odulatb  17529  oduclatb  17530  posglbmo  17533  resscntz  18147  oppgid  18169  gsumcom  18762  dfrhm2  19106  lsslss  19356  fiidomfld  19705  opsrtoslem1  19880  xrsdsreclb  20189  znleval  20298  gsumcom3  20609  madutpos  20853  fvmptnn04if  21061  ntreq0  21289  restopn2  21389  ist0-3  21557  1stcelcls  21673  txkgen  21864  trfil2  22099  elflim2  22176  flimrest  22195  txflf  22218  fclsrest  22236  tsmssubm  22354  ismet2  22546  blres  22644  metrest  22737  restmetu  22783  xrtgioo  23017  elii1  23142  isclmp  23304  isncvsngp  23356  evthicc2  23664  ovolfcl  23670  dyaddisj  23800  mbfaddlem  23864  itg1climres  23918  mbfi1fseqlem4  23922  iblpos  23996  itgposval  23999  ditgsplit  24062  ellimc3  24080  itgsubst  24249  deg1ldg  24289  sincosq1sgn  24688  sincosq3sgn  24690  cos11  24717  dvdsflsumcom  25366  fsumvma  25390  logfaclbnd  25399  dchrelbas3  25415  lgsdi  25511  lgsquadlem1  25557  lgsquadlem2  25558  lgsquadlem3  25559  2lgslem1a  25568  istrkg2ld  25811  tgjustf  25824  tgcgr4  25882  mirreu3  26005  hpgcom  26115  colhp  26118  dfcgra2  26178  nbgrel  26687  nbgrsym  26710  wlkson  27003  isspthonpth  27101  usgr2pth0  27117  wwlksnextinj  27263  wwlksnextinjOLD  27268  elwspths2spth  27347  rusgrnumwwlkl1  27348  clwwlknclwwlkdifnum  27360  clwwlkn1  27431  clwwlkn2  27434  0clwlk  27533  iseupthf1o  27605  eupth2lem2  27623  frgrncvvdeqlem2  27708  fusgr2wsp2nb  27742  fusgreg2wsp  27744  numclwwlkqhash  27803  frgrreg  27826  frgrregord013  27827  h2hcau  28408  nmopub  29339  nmfnleub  29356  chrelati  29795  cvexchlem  29799  mdsymlem8  29841  sumdmdii  29846  spc2ed  29884  difrab2  29901  2ndpreima  30051  fpwrelmapffslem  30073  xrofsup  30098  pmtrprfv2  30446  smatrcl  30460  cnvordtrestixx  30557  issgon  30784  eulerpartlemr  31034  eulerpartlemgvv  31036  ballotlem2  31149  sgn3da  31202  oddprm2  31335  bnj257  31375  bnj545  31564  bnj594  31581  coep  32235  dfpo2  32239  dfdm5  32264  dfrn5  32265  elima4  32267  frpoind  32329  frind  32332  sletri3  32469  nocvxmin  32483  sltrec  32513  elfix  32599  dffix2  32601  sscoid  32609  brimg  32633  brsuccf  32637  dfrecs2  32646  dfrdg4  32647  cgrcomlr  32694  ofscom  32703  btwnexch  32721  fscgr  32776  bj-dfifc2  33143  bj-restuni  33623  bj-0int  33628  bj-dfmpt2a  33644  bj-eldiag  33670  bj-ccinftydisj  33690  mptsnunlem  33781  topdifinffinlem  33790  wl-cases2-dnf  33890  wl-ax11-lem4  33959  fin2solem  34020  poimirlem4  34039  poimirlem26  34061  poimirlem30  34065  poimirlem32  34067  ftc1anclem6  34115  ftc1anc  34118  heibor1  34233  isdrngo3  34382  isdmn3  34497  an2anr  34636  anan  34637  inxpxrn  34781  prtlem70  35011  lrelat  35168  islshpat  35171  atlrelat1  35475  ishlat2  35507  pmapglb  35924  polval2N  36060  cdlemb3  36760  diblsmopel  37325  dicelval3  37334  diclspsn  37348  fz1eqin  38292  diophrex  38299  fphpd  38340  fzneg  38508  expdioph  38549  dford4  38555  lnr2i  38645  fgraphopab  38747  ifpancor  38766  ifpdfbi  38776  ifpidg  38794  ifpid2g  38796  ifpid1g  38797  ifpim23g  38798  ifp1bi  38805  rp-fakeoranass  38817  dfid7  38876  dfrtrcl5  38893  relexp0eq  38950  fsovrfovd  39259  rcompleq  39274  uunT1p1  39950  uun132p1  39955  un2122  39959  uun2131p1  39961  uunT12p1  39969  uunT12p2  39970  uunT12p3  39971  uun2221  39982  uun2221p1  39983  uun2221p2  39984  3impdirp1  39985  ancomstVD  40034  icccncfext  41028  dvnmul  41086  dvmptfprodlem  41087  dvnprodlem2  41090  fourierdlem42  41293  fourierdlem83  41333  2reu3  42149  2reu7  42152  2reu8  42153  2reuimp0  42155  ndmaovcom  42246  an4com24  42309  4an21  42311  sprvalpwn0  42422  prpair  42440  prproropf1olem0  42441  2zrngnmrid  42965  opeliun2xp  43126  eliunxp2  43127  rrx2linest  43478