Theorem ancom 437

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 436	. 2 ⊢ ((φ ∧ ψ) → (ψ ∧ φ))
2		pm3.22 436	. 2 ⊢ ((ψ ∧ φ) → (φ ∧ ψ))
3	1, 2	impbii 180	1 ⊢ ((φ ∧ ψ) ↔ (ψ ∧ φ))

Syntax hints:   ↔ wb 176   ∧ wa 358

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 177  df-an 360

This theorem is referenced by:  ancomd  438  ancomsd  440  pm4.71r  612  pm5.32ri  619  pm5.32rd  621  anbi2ci  677  anbi12ci  679  an12  772  an32  773  an13  774  an42  798  andir  838  dfbi3  863  rbaib  873  rbaibr  874  3anrot  939  3ancoma  941  nancom  1290  excxor  1309  ancomsimp  1369  cador  1391  cadcoma  1395  cadcomb  1396  cad1  1398  exancom  1586  19.42  1880  eu1  2225  moaneu  2263  moanmo  2264  2eu3  2286  2eu6  2289  2eu7  2290  2eu8  2291  eq2tri  2412  r19.28av  2754  r19.29r  2756  r19.42v  2766  rexcomf  2771  rabswap  2791  euxfr2  3022  rmo4  3030  reu8  3033  rmo3  3134  incom  3449  difin2  3517  difin0ss  3617  ssunsn  3867  pw1in  4165  eluni1g  4173  elxpk2  4198  opkelcokg  4262  opkelimagekg  4272  cnvkxpk  4277  sikexlem  4296  dfpw12  4302  insklem  4305  unipw1  4326  addcass  4416  nnsucelrlem1  4425  nnsucelrlem2  4426  ltfinex  4465  ssfin  4471  dfop2lem1  4574  eqvinop  4607  opeq  4620  setconslem1  4732  setconslem2  4733  setconslem4  4735  elswap  4741  dfid3  4769  brinxp2  4836  brswap2  4861  cnvco  4895  dmuni  4915  dfima3  4952  elres  4996  dfres2  5003  imai  5011  rnuni  5039  cnvxp  5044  dmsnopg  5067  cnvsn  5074  rnco  5088  df2nd2  5112  fncnv  5159  fununi  5161  fnres  5200  fnopabg  5206  f1funfun  5264  dff1o2  5292  f1ocnvb  5299  eqfnfv3  5395  respreima  5411  fsn  5433  isoini  5498  opbr1st  5502  cnvswap  5511  swapf1o  5512  dmsi  5520  ndmovcom  5618  mptpreima  5683  trtxp  5782  brtxp  5784  elfix  5788  brimage  5794  oqelins4  5795  funsex  5829  pw1fnex  5853  clos1induct  5881  clos1is  5882  transex  5911  antisymex  5913  pmvalg  6011  elpmg  6014  mapval2  6019  enpw1lem1  6062  enmap2lem1  6064  enmap1lem1  6070  lecex  6116  ovmuc  6131  tcfnex  6245  addccan2nclem1  6264  nmembers1lem1  6269  nnc3n3p1  6279  spacvallem1  6282  spacis  6289  nchoicelem10  6299  nchoicelem11  6300  nchoicelem16  6305