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  563  an32  564  an13  565  an42  589  andir  827  rbaib  929  rbaibr  930  ifptru  998  ifpfal  999  3anrot  1010  3ancoma  1012  excxor  1423  xorcom  1433  xordc  1437  xordc1  1438  dfbi3dc  1442  ancomsimp  1486  exancom  1657  19.29r  1670  19.42h  1735  19.42  1736  eu1  2104  moaneu  2156  moanmo  2157  2eu7  2174  eq2tri  2291  r19.28av  2670  r19.29r  2672  r19.42v  2691  rexcomf  2696  rabswap  2713  euxfr2dc  2992  rmo4  3000  reu8  3003  rmo3f  3004  rmo3  3125  incom  3401  difin2  3471  symdifxor  3475  elif  3621  inuni  4250  eqvinop  4341  uniuni  4554  dtruex  4663  elvvv  4795  brinxp2  4799  dmuni  4947  dfres2  5071  dfima2  5084  imadmrn  5092  imai  5099  cnvxp  5162  cnvcnvsn  5220  mptpreima  5237  rnco  5250  unixpm  5279  ressn  5284  xpcom  5290  fncnv  5403  fununi  5405  imadiflem  5416  fnres  5456  fnopabg  5463  dff1o2  5597  eqfnfv3  5755  respreima  5783  fsn  5827  fliftcnv  5946  isoini  5969  spc2ed  6407  brtpos2  6460  tpostpos  6473  tposmpo  6490  nnaord  6720  pmex  6865  elpmg  6876  mapval2  6890  mapsnen  7029  map1  7030  xpsnen  7048  xpcomco  7053  elfi2  7214  supmoti  7235  cnvti  7261  2omotaplemap  7519  elni2  7577  enq0enq  7694  prltlu  7750  prnmaxl  7751  prnminu  7752  nqprrnd  7806  ltpopr  7858  letri3  8302  lesub0  8701  creur  9181  xrletri3  10083  iooneg  10267  iccneg  10268  elfzuzb  10299  fzrev  10364  redivap  11497  imdivap  11504  rersqreu  11651  lenegsq  11718  climrecvg1n  11971  fisumcom2  12062  fsumcom  12063  fprodcom2fi  12250  fprodcom  12251  gcdcom  12607  bezoutlembi  12639  dfgcd2  12648  lcmcom  12699  isprm2  12752  unennn  13081  dfrhm2  14232  issubrng  14277  ntreq0  14926  restopn2  14977  ismet2  15148  blres  15228  metrest  15300  dedekindicclemicc  15426  sincosq3sgn  15622  lgsdi  15839  lgsquadlem3  15881  2lgslem1a  15890  clwwlkn1  16342  clwwlkn2  16345  iseupthf1o  16372  eupth2lem2dc  16383