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  2753  r19.29r  2755  r19.42v  2765  rexcomf  2770  rabswap  2790  euxfr2  3021  rmo4  3029  reu8  3032  rmo3  3133  incom  3448  difin2  3516  difin0ss  3616  ssunsn  3866  pw1in  4164  eluni1g  4172  elxpk2  4197  opkelcokg  4261  opkelimagekg  4271  cnvkxpk  4276  sikexlem  4295  dfpw12  4301  insklem  4304  unipw1  4325  addcass  4415  nnsucelrlem1  4424  nnsucelrlem2  4425  ltfinex  4464  ssfin  4470  dfop2lem1  4573  eqvinop  4606  opeq  4619  setconslem1  4731  setconslem2  4732  setconslem4  4734  elswap  4740  dfid3  4768  brinxp2  4835  brswap2  4860  cnvco  4894  dmuni  4914  dfima3  4951  elres  4995  dfres2  5002  imai  5010  rnuni  5038  cnvxp  5043  dmsnopg  5066  cnvsn  5073  rnco  5087  df2nd2  5111  fncnv  5158  fununi  5160  fnres  5199  fnopabg  5205  f1funfun  5263  dff1o2  5291  f1ocnvb  5298  eqfnfv3  5394  respreima  5410  fsn  5432  isoini  5497  opbr1st  5501  cnvswap  5510  swapf1o  5511  dmsi  5519  ndmovcom  5617  mptpreima  5682  trtxp  5781  brtxp  5783  elfix  5787  brimage  5793  oqelins4  5794  funsex  5828  pw1fnex  5852  clos1induct  5880  clos1is  5881  transex  5910  antisymex  5912  pmvalg  6010  elpmg  6013  mapval2  6018  enpw1lem1  6061  enmap2lem1  6063  enmap1lem1  6069  lecex  6115  ovmuc  6130  tcfnex  6244  addccan2nclem1  6263  nmembers1lem1  6268  nnc3n3p1  6278  spacvallem1  6281  spacis  6288  nchoicelem10  6298  nchoicelem11  6299  nchoicelem16  6304