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  821  rbaib  923  rbaibr  924  3anrot  986  3ancoma  988  excxor  1398  xorcom  1408  xordc  1412  xordc1  1413  dfbi3dc  1417  ancomsimp  1461  exancom  1632  19.29r  1645  19.42h  1711  19.42  1712  eu1  2080  moaneu  2131  moanmo  2132  2eu7  2149  eq2tri  2266  r19.28av  2643  r19.29r  2645  r19.42v  2664  rexcomf  2669  rabswap  2686  euxfr2dc  2962  rmo4  2970  reu8  2973  rmo3f  2974  rmo3  3094  incom  3369  difin2  3439  symdifxor  3443  elif  3587  inuni  4207  eqvinop  4295  uniuni  4506  dtruex  4615  elvvv  4746  brinxp2  4750  dmuni  4897  dfres2  5020  dfima2  5033  imadmrn  5041  imai  5047  cnvxp  5110  cnvcnvsn  5168  mptpreima  5185  rnco  5198  unixpm  5227  ressn  5232  xpcom  5238  fncnv  5349  fununi  5351  imadiflem  5362  fnres  5402  fnopabg  5409  dff1o2  5539  eqfnfv3  5692  respreima  5721  fsn  5765  fliftcnv  5877  isoini  5900  spc2ed  6332  brtpos2  6350  tpostpos  6363  tposmpo  6380  nnaord  6608  pmex  6753  elpmg  6764  mapval2  6778  mapsnen  6917  map1  6918  xpsnen  6931  xpcomco  6936  elfi2  7089  supmoti  7110  cnvti  7136  2omotaplemap  7389  elni2  7447  enq0enq  7564  prltlu  7620  prnmaxl  7621  prnminu  7622  nqprrnd  7676  ltpopr  7728  letri3  8173  lesub0  8572  creur  9052  xrletri3  9946  iooneg  10130  iccneg  10131  elfzuzb  10161  fzrev  10226  redivap  11260  imdivap  11267  rersqreu  11414  lenegsq  11481  climrecvg1n  11734  fisumcom2  11824  fsumcom  11825  fprodcom2fi  12012  fprodcom  12013  gcdcom  12369  bezoutlembi  12401  dfgcd2  12410  lcmcom  12461  isprm2  12514  unennn  12843  dfrhm2  13991  issubrng  14036  ntreq0  14679  restopn2  14730  ismet2  14901  blres  14981  metrest  15053  dedekindicclemicc  15179  sincosq3sgn  15375  lgsdi  15589  lgsquadlem3  15631  2lgslem1a  15640