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-mp 5  ax-1 6  ax-2 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  biancomi  268  biancomd  269  pm4.71r  388  pm5.32rd  447  pm5.32ri  451  anbi2ci  455  anbi12ci  457  mpan10  466  an12  551  an32  552  an13  553  an42  577  andir  809  rbaib  911  rbaibr  912  3anrot  973  3ancoma  975  excxor  1368  xorcom  1378  xordc  1382  xordc1  1383  dfbi3dc  1387  ancomsimp  1428  exancom  1596  19.29r  1609  19.42h  1675  19.42  1676  eu1  2039  moaneu  2090  moanmo  2091  2eu7  2108  eq2tri  2226  r19.28av  2602  r19.29r  2604  r19.42v  2623  rexcomf  2628  rabswap  2644  euxfr2dc  2911  rmo4  2919  reu8  2922  rmo3f  2923  rmo3  3042  incom  3314  difin2  3384  symdifxor  3388  inuni  4134  eqvinop  4221  uniuni  4429  dtruex  4536  elvvv  4667  brinxp2  4671  dmuni  4814  dfres2  4936  dfima2  4948  imadmrn  4956  imai  4960  cnvxp  5022  cnvcnvsn  5080  mptpreima  5097  rnco  5110  unixpm  5139  ressn  5144  xpcom  5150  fncnv  5254  fununi  5256  imadiflem  5267  fnres  5304  fnopabg  5311  dff1o2  5437  eqfnfv3  5585  respreima  5613  fsn  5657  fliftcnv  5763  isoini  5786  spc2ed  6201  brtpos2  6219  tpostpos  6232  tposmpo  6249  nnaord  6477  pmex  6619  elpmg  6630  mapval2  6644  mapsnen  6777  map1  6778  xpsnen  6787  xpcomco  6792  elfi2  6937  supmoti  6958  cnvti  6984  elni2  7255  enq0enq  7372  prltlu  7428  prnmaxl  7429  prnminu  7430  nqprrnd  7484  ltpopr  7536  letri3  7979  lesub0  8377  creur  8854  xrletri3  9740  iooneg  9924  iccneg  9925  elfzuzb  9954  fzrev  10019  redivap  10816  imdivap  10823  rersqreu  10970  lenegsq  11037  climrecvg1n  11289  fisumcom2  11379  fsumcom  11380  fprodcom2fi  11567  fprodcom  11568  gcdcom  11906  bezoutlembi  11938  dfgcd2  11947  lcmcom  11996  isprm2  12049  unennn  12330  ntreq0  12772  restopn2  12823  ismet2  12994  blres  13074  metrest  13146  dedekindicclemicc  13250  sincosq3sgn  13389  lgsdi  13578