Theorem ancom 264

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

Syntax hints:   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ancomd  265  ancomsd  267  biancomi  268  biancomd  269  pm4.71r  388  pm5.32rd  448  pm5.32ri  452  anbi2ci  456  anbi12ci  458  bianassc  467  mpan10  471  an12  556  an32  557  an13  558  an42  582  andir  814  rbaib  916  rbaibr  917  3anrot  978  3ancoma  980  excxor  1373  xorcom  1383  xordc  1387  xordc1  1388  dfbi3dc  1392  ancomsimp  1433  exancom  1601  19.29r  1614  19.42h  1680  19.42  1681  eu1  2044  moaneu  2095  moanmo  2096  2eu7  2113  eq2tri  2230  r19.28av  2606  r19.29r  2608  r19.42v  2627  rexcomf  2632  rabswap  2648  euxfr2dc  2915  rmo4  2923  reu8  2926  rmo3f  2927  rmo3  3046  incom  3319  difin2  3389  symdifxor  3393  inuni  4141  eqvinop  4228  uniuni  4436  dtruex  4543  elvvv  4674  brinxp2  4678  dmuni  4821  dfres2  4943  dfima2  4955  imadmrn  4963  imai  4967  cnvxp  5029  cnvcnvsn  5087  mptpreima  5104  rnco  5117  unixpm  5146  ressn  5151  xpcom  5157  fncnv  5264  fununi  5266  imadiflem  5277  fnres  5314  fnopabg  5321  dff1o2  5447  eqfnfv3  5595  respreima  5624  fsn  5668  fliftcnv  5774  isoini  5797  spc2ed  6212  brtpos2  6230  tpostpos  6243  tposmpo  6260  nnaord  6488  pmex  6631  elpmg  6642  mapval2  6656  mapsnen  6789  map1  6790  xpsnen  6799  xpcomco  6804  elfi2  6949  supmoti  6970  cnvti  6996  elni2  7276  enq0enq  7393  prltlu  7449  prnmaxl  7450  prnminu  7451  nqprrnd  7505  ltpopr  7557  letri3  8000  lesub0  8398  creur  8875  xrletri3  9761  iooneg  9945  iccneg  9946  elfzuzb  9975  fzrev  10040  redivap  10838  imdivap  10845  rersqreu  10992  lenegsq  11059  climrecvg1n  11311  fisumcom2  11401  fsumcom  11402  fprodcom2fi  11589  fprodcom  11590  gcdcom  11928  bezoutlembi  11960  dfgcd2  11969  lcmcom  12018  isprm2  12071  unennn  12352  ntreq0  12926  restopn2  12977  ismet2  13148  blres  13228  metrest  13300  dedekindicclemicc  13404  sincosq3sgn  13543  lgsdi  13732