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  5935  isoini  5958  spc2ed  6397  brtpos2  6416  tpostpos  6429  tposmpo  6446  nnaord  6676  pmex  6821  elpmg  6832  mapval2  6846  mapsnen  6985  map1  6986  xpsnen  7004  xpcomco  7009  elfi2  7170  supmoti  7191  cnvti  7217  2omotaplemap  7475  elni2  7533  enq0enq  7650  prltlu  7706  prnmaxl  7707  prnminu  7708  nqprrnd  7762  ltpopr  7814  letri3  8259  lesub0  8658  creur  9138  xrletri3  10038  iooneg  10222  iccneg  10223  elfzuzb  10253  fzrev  10318  redivap  11434  imdivap  11441  rersqreu  11588  lenegsq  11655  climrecvg1n  11908  fisumcom2  11998  fsumcom  11999  fprodcom2fi  12186  fprodcom  12187  gcdcom  12543  bezoutlembi  12575  dfgcd2  12584  lcmcom  12635  isprm2  12688  unennn  13017  dfrhm2  14167  issubrng  14212  ntreq0  14855  restopn2  14906  ismet2  15077  blres  15157  metrest  15229  dedekindicclemicc  15355  sincosq3sgn  15551  lgsdi  15765  lgsquadlem3  15807  2lgslem1a  15816  clwwlkn1  16268  clwwlkn2  16271  iseupthf1o  16298  eupth2lem2dc  16309