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  2723  euxfr2dc  3002  rmo4  3010  reu8  3013  rmo3f  3014  rmo3  3135  incom  3411  difin2  3483  symdifxor  3487  elif  3634  inuni  4267  eqvinop  4359  uniuni  4572  dtruex  4681  elvvv  4813  brinxp2  4817  dmuni  4966  dfres2  5090  dfima2  5103  imadmrn  5111  imai  5118  cnvxp  5181  cnvcnvsn  5239  mptpreima  5256  rnco  5269  unixpm  5298  ressn  5303  xpcom  5309  fncnv  5422  fununi  5424  imadiflem  5435  fnres  5475  fnopabg  5482  dff1o2  5619  eqfnfv3  5777  respreima  5805  fsn  5849  fliftcnv  5968  isoini  5991  spc2ed  6429  brtpos2  6482  tpostpos  6495  tposmpo  6512  nnaord  6742  pmex  6887  elpmg  6898  mapval2  6912  mapsnend  7052  mapsnen  7053  map1  7054  xpsnen  7072  xpcomco  7077  elfi2  7259  supmoti  7284  cnvti  7310  2omotaplemap  7571  elni2  7629  enq0enq  7746  prltlu  7802  prnmaxl  7803  prnminu  7804  nqprrnd  7858  ltpopr  7910  letri3  8354  lesub0  8753  creur  9233  xrletri3  10137  iooneg  10321  iccneg  10322  elfzuzb  10353  fzrev  10418  redivap  11559  imdivap  11566  rersqreu  11713  lenegsq  11780  climrecvg1n  12033  fisumcom2  12124  fsumcom  12125  fprodcom2fi  12312  fprodcom  12313  gcdcom  12669  bezoutlembi  12701  dfgcd2  12710  lcmcom  12761  isprm2  12814  ballotfilem2  13142  unennn  13148  dfrhm2  14299  issubrng  14344  ntreq0  14997  restopn2  15048  ismet2  15219  blres  15299  metrest  15371  dedekindicclemicc  15497  sincosq3sgn  15693  lgsdi  15910  lgsquadlem3  15952  2lgslem1a  15961  clwwlkn1  16413  clwwlkn2  16416  iseupthf1o  16443  eupth2lem2dc  16454