Theorem ancom 264

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

Syntax hints:   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ancomd  265  ancomsd  267  pm4.71r  385  pm5.32rd  442  pm5.32ri  446  anbi2ci  450  anbi12ci  452  mpan10  461  an12  531  an32  532  an13  533  an42  557  andir  774  rbaib  874  rbaibr  875  3anrot  935  3ancoma  937  excxor  1324  xorcom  1334  xordc  1338  xordc1  1339  dfbi3dc  1343  ancomsimp  1384  exancom  1555  19.29r  1568  19.42h  1633  19.42  1634  eu1  1985  moaneu  2036  moanmo  2037  2eu7  2054  eq2tri  2159  r19.28av  2527  r19.29r  2529  r19.42v  2546  rexcomf  2551  rabswap  2567  euxfr2dc  2822  rmo4  2830  reu8  2833  rmo3f  2834  rmo3  2952  incom  3215  difin2  3285  symdifxor  3289  inuni  4020  eqvinop  4103  uniuni  4310  dtruex  4412  elvvv  4540  brinxp2  4544  dmuni  4687  dfres2  4807  dfima2  4819  imadmrn  4827  imai  4831  cnvxp  4893  cnvcnvsn  4951  mptpreima  4968  rnco  4981  unixpm  5010  ressn  5015  xpcom  5021  fncnv  5125  fununi  5127  imadiflem  5138  fnres  5175  fnopabg  5182  dff1o2  5306  eqfnfv3  5452  respreima  5480  fsn  5524  fliftcnv  5628  isoini  5651  spc2ed  6060  brtpos2  6078  tpostpos  6091  tposmpo  6108  nnaord  6335  pmex  6477  elpmg  6488  mapval2  6502  mapsnen  6635  map1  6636  xpsnen  6644  xpcomco  6649  supmoti  6795  cnvti  6821  elni2  7023  enq0enq  7140  prltlu  7196  prnmaxl  7197  prnminu  7198  nqprrnd  7252  ltpopr  7304  letri3  7716  lesub0  8108  creur  8575  xrletri3  9429  iooneg  9612  iccneg  9613  elfzuzb  9641  fzrev  9705  redivap  10487  imdivap  10494  rersqreu  10640  lenegsq  10707  climrecvg1n  10956  fisumcom2  11046  fsumcom  11047  gcdcom  11457  bezoutlembi  11486  dfgcd2  11495  lcmcom  11538  isprm2  11591  unennn  11702  ntreq0  12083  restopn2  12134  ismet2  12282  blres  12362  metrest  12434