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  394  pm5.32rd  455  pm5.32ri  459  anbi2ci  463  anbi12ci  465  bianassc  474  mpan10  478  an12  567  an32  568  an13  569  an42  593  andir  831  rbaib  933  rbaibr  934  ifptru  1002  ifpfal  1003  3anrot  1014  3ancoma  1016  excxor  1427  xorcom  1437  xordc  1441  xordc1  1442  dfbi3dc  1446  ancomsimp  1490  exancom  1661  19.29r  1674  19.42h  1739  19.42  1740  eu1  2111  moaneu  2163  moanmo  2164  2eu7  2181  eq2tri  2298  r19.28av  2687  r19.29r  2689  r19.42v  2708  rexcomf  2713  rabswap  2731  euxfr2dc  3011  rmo4  3019  reu8  3022  rmo3f  3023  rmo3  3144  incom  3421  difin2  3493  symdifxor  3497  elif  3649  inuni  4286  eqvinop  4378  uniuni  4592  dtruex  4701  elvvv  4833  brinxp2  4837  dmuni  4986  dfres2  5110  dfima2  5123  imadmrn  5131  imai  5138  cnvxp  5201  cnvcnvsn  5259  mptpreima  5276  rnco  5289  unixpm  5318  ressn  5323  xpcom  5329  fncnv  5442  fununi  5444  imadiflem  5455  fnres  5495  fnopabg  5502  dff1o2  5639  eqfnfv3  5799  respreima  5827  fsn  5871  fliftcnv  5991  isoini  6014  spc2ed  6459  brtpos2  6512  tpostpos  6525  tposmpo  6542  nnaord  6772  pmex  6917  elpmg  6928  mapval2  6949  mapsnend  7089  mapsnen  7090  map1  7091  xpsnen  7109  xpcomco  7114  elfi2  7296  supmoti  7323  cnvti  7349  2omotaplemap  7613  elni2  7671  enq0enq  7788  prltlu  7844  prnmaxl  7845  prnminu  7846  nqprrnd  7900  ltpopr  7952  letri3  8396  lesub0  8797  creur  9279  xrletri3  10185  iooneg  10369  iccneg  10370  elfzuzb  10401  fzrev  10469  redivap  11617  imdivap  11624  rersqreu  11772  lenegsq  11839  climrecvg1n  12092  fisumcom2  12183  fsumcom  12184  fprodcom2fi  12371  fprodcom  12372  gcdcom  12728  bezoutlembi  12760  dfgcd2  12769  lcmcom  12820  isprm2  12873  ballotfilem2  13206  unennn  13266  dfrhm2  14434  issubrng  14480  ntreq0  15156  restopn2  15207  ismet2  15378  blres  15458  metrest  15530  dedekindicclemicc  15656  sincosq3sgn  15852  lgsdi  16070  lgsquadlem3  16112  2lgslem1a  16121  clwwlkn1  16573  clwwlkn2  16576  iseupthf1o  16603  eupth2lem2dc  16614