Theorem ancom 266

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

Syntax hints:   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ancomd  267  ancomsd  269  biancomi  270  biancomd  271  pm4.71r  390  pm5.32rd  451  pm5.32ri  455  anbi2ci  459  anbi12ci  461  bianassc  470  mpan10  474  an12  561  an32  562  an13  563  an42  587  andir  824  rbaib  926  rbaibr  927  ifptru  995  ifpfal  996  3anrot  1007  3ancoma  1009  excxor  1420  xorcom  1430  xordc  1434  xordc1  1435  dfbi3dc  1439  ancomsimp  1483  exancom  1654  19.29r  1667  19.42h  1733  19.42  1734  eu1  2102  moaneu  2154  moanmo  2155  2eu7  2172  eq2tri  2289  r19.28av  2667  r19.29r  2669  r19.42v  2688  rexcomf  2693  rabswap  2710  euxfr2dc  2988  rmo4  2996  reu8  2999  rmo3f  3000  rmo3  3121  incom  3396  difin2  3466  symdifxor  3470  elif  3614  inuni  4238  eqvinop  4328  uniuni  4541  dtruex  4650  elvvv  4781  brinxp2  4785  dmuni  4932  dfres2  5056  dfima2  5069  imadmrn  5077  imai  5083  cnvxp  5146  cnvcnvsn  5204  mptpreima  5221  rnco  5234  unixpm  5263  ressn  5268  xpcom  5274  fncnv  5386  fununi  5388  imadiflem  5399  fnres  5439  fnopabg  5446  dff1o2  5576  eqfnfv3  5733  respreima  5762  fsn  5806  fliftcnv  5918  isoini  5941  spc2ed  6377  brtpos2  6395  tpostpos  6408  tposmpo  6425  nnaord  6653  pmex  6798  elpmg  6809  mapval2  6823  mapsnen  6962  map1  6963  xpsnen  6976  xpcomco  6981  elfi2  7135  supmoti  7156  cnvti  7182  2omotaplemap  7439  elni2  7497  enq0enq  7614  prltlu  7670  prnmaxl  7671  prnminu  7672  nqprrnd  7726  ltpopr  7778  letri3  8223  lesub0  8622  creur  9102  xrletri3  9996  iooneg  10180  iccneg  10181  elfzuzb  10211  fzrev  10276  redivap  11380  imdivap  11387  rersqreu  11534  lenegsq  11601  climrecvg1n  11854  fisumcom2  11944  fsumcom  11945  fprodcom2fi  12132  fprodcom  12133  gcdcom  12489  bezoutlembi  12521  dfgcd2  12530  lcmcom  12581  isprm2  12634  unennn  12963  dfrhm2  14112  issubrng  14157  ntreq0  14800  restopn2  14851  ismet2  15022  blres  15102  metrest  15174  dedekindicclemicc  15300  sincosq3sgn  15496  lgsdi  15710  lgsquadlem3  15752  2lgslem1a  15761