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  2105  moaneu  2157  moanmo  2158  2eu7  2175  eq2tri  2292  r19.28av  2679  r19.29r  2681  r19.42v  2700  rexcomf  2705  rabswap  2722  euxfr2dc  3001  rmo4  3009  reu8  3012  rmo3f  3013  rmo3  3134  incom  3410  difin2  3482  symdifxor  3486  elif  3633  inuni  4266  eqvinop  4358  uniuni  4571  dtruex  4680  elvvv  4812  brinxp2  4816  dmuni  4965  dfres2  5089  dfima2  5102  imadmrn  5110  imai  5117  cnvxp  5180  cnvcnvsn  5238  mptpreima  5255  rnco  5268  unixpm  5297  ressn  5302  xpcom  5308  fncnv  5421  fununi  5423  imadiflem  5434  fnres  5474  fnopabg  5481  dff1o2  5618  eqfnfv3  5776  respreima  5804  fsn  5848  fliftcnv  5967  isoini  5990  spc2ed  6428  brtpos2  6481  tpostpos  6494  tposmpo  6511  nnaord  6741  pmex  6886  elpmg  6897  mapval2  6911  mapsnend  7051  mapsnen  7052  map1  7053  xpsnen  7071  xpcomco  7076  elfi2  7258  supmoti  7283  cnvti  7309  2omotaplemap  7570  elni2  7628  enq0enq  7745  prltlu  7801  prnmaxl  7802  prnminu  7803  nqprrnd  7857  ltpopr  7909  letri3  8353  lesub0  8752  creur  9232  xrletri3  10136  iooneg  10320  iccneg  10321  elfzuzb  10352  fzrev  10417  redivap  11555  imdivap  11562  rersqreu  11709  lenegsq  11776  climrecvg1n  12029  fisumcom2  12120  fsumcom  12121  fprodcom2fi  12308  fprodcom  12309  gcdcom  12665  bezoutlembi  12697  dfgcd2  12706  lcmcom  12757  isprm2  12810  unennn  13140  dfrhm2  14291  issubrng  14336  ntreq0  14989  restopn2  15040  ismet2  15211  blres  15291  metrest  15363  dedekindicclemicc  15489  sincosq3sgn  15685  lgsdi  15902  lgsquadlem3  15944  2lgslem1a  15953  clwwlkn1  16405  clwwlkn2  16408  iseupthf1o  16435  eupth2lem2dc  16446