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  826  rbaib  928  rbaibr  929  ifptru  997  ifpfal  998  3anrot  1009  3ancoma  1011  excxor  1422  xorcom  1432  xordc  1436  xordc1  1437  dfbi3dc  1441  ancomsimp  1485  exancom  1656  19.29r  1669  19.42h  1735  19.42  1736  eu1  2104  moaneu  2156  moanmo  2157  2eu7  2174  eq2tri  2291  r19.28av  2669  r19.29r  2671  r19.42v  2690  rexcomf  2695  rabswap  2712  euxfr2dc  2991  rmo4  2999  reu8  3002  rmo3f  3003  rmo3  3124  incom  3399  difin2  3469  symdifxor  3473  elif  3617  inuni  4245  eqvinop  4335  uniuni  4548  dtruex  4657  elvvv  4789  brinxp2  4793  dmuni  4941  dfres2  5065  dfima2  5078  imadmrn  5086  imai  5092  cnvxp  5155  cnvcnvsn  5213  mptpreima  5230  rnco  5243  unixpm  5272  ressn  5277  xpcom  5283  fncnv  5396  fununi  5398  imadiflem  5409  fnres  5449  fnopabg  5456  dff1o2  5588  eqfnfv3  5746  respreima  5775  fsn  5819  fliftcnv  5936  isoini  5959  spc2ed  6398  brtpos2  6417  tpostpos  6430  tposmpo  6447  nnaord  6677  pmex  6822  elpmg  6833  mapval2  6847  mapsnen  6986  map1  6987  xpsnen  7005  xpcomco  7010  elfi2  7171  supmoti  7192  cnvti  7218  2omotaplemap  7476  elni2  7534  enq0enq  7651  prltlu  7707  prnmaxl  7708  prnminu  7709  nqprrnd  7763  ltpopr  7815  letri3  8260  lesub0  8659  creur  9139  xrletri3  10039  iooneg  10223  iccneg  10224  elfzuzb  10254  fzrev  10319  redivap  11439  imdivap  11446  rersqreu  11593  lenegsq  11660  climrecvg1n  11913  fisumcom2  12004  fsumcom  12005  fprodcom2fi  12192  fprodcom  12193  gcdcom  12549  bezoutlembi  12581  dfgcd2  12590  lcmcom  12641  isprm2  12694  unennn  13023  dfrhm2  14174  issubrng  14219  ntreq0  14862  restopn2  14913  ismet2  15084  blres  15164  metrest  15236  dedekindicclemicc  15362  sincosq3sgn  15558  lgsdi  15772  lgsquadlem3  15814  2lgslem1a  15823  clwwlkn1  16275  clwwlkn2  16278  iseupthf1o  16305  eupth2lem2dc  16316