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  4239  eqvinop  4329  uniuni  4542  dtruex  4651  elvvv  4782  brinxp2  4786  dmuni  4933  dfres2  5057  dfima2  5070  imadmrn  5078  imai  5084  cnvxp  5147  cnvcnvsn  5205  mptpreima  5222  rnco  5235  unixpm  5264  ressn  5269  xpcom  5275  fncnv  5387  fununi  5389  imadiflem  5400  fnres  5440  fnopabg  5447  dff1o2  5579  eqfnfv3  5736  respreima  5765  fsn  5809  fliftcnv  5925  isoini  5948  spc2ed  6385  brtpos2  6403  tpostpos  6416  tposmpo  6433  nnaord  6663  pmex  6808  elpmg  6819  mapval2  6833  mapsnen  6972  map1  6973  xpsnen  6988  xpcomco  6993  elfi2  7150  supmoti  7171  cnvti  7197  2omotaplemap  7454  elni2  7512  enq0enq  7629  prltlu  7685  prnmaxl  7686  prnminu  7687  nqprrnd  7741  ltpopr  7793  letri3  8238  lesub0  8637  creur  9117  xrletri3  10012  iooneg  10196  iccneg  10197  elfzuzb  10227  fzrev  10292  redivap  11400  imdivap  11407  rersqreu  11554  lenegsq  11621  climrecvg1n  11874  fisumcom2  11964  fsumcom  11965  fprodcom2fi  12152  fprodcom  12153  gcdcom  12509  bezoutlembi  12541  dfgcd2  12550  lcmcom  12601  isprm2  12654  unennn  12983  dfrhm2  14133  issubrng  14178  ntreq0  14821  restopn2  14872  ismet2  15043  blres  15123  metrest  15195  dedekindicclemicc  15321  sincosq3sgn  15517  lgsdi  15731  lgsquadlem3  15773  2lgslem1a  15782