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  561  an32  562  an13  563  an42  587  andir  820  rbaib  922  rbaibr  923  3anrot  985  3ancoma  987  excxor  1397  xorcom  1407  xordc  1411  xordc1  1412  dfbi3dc  1416  ancomsimp  1459  exancom  1630  19.29r  1643  19.42h  1709  19.42  1710  eu1  2078  moaneu  2129  moanmo  2130  2eu7  2147  eq2tri  2264  r19.28av  2641  r19.29r  2643  r19.42v  2662  rexcomf  2667  rabswap  2684  euxfr2dc  2957  rmo4  2965  reu8  2968  rmo3f  2969  rmo3  3089  incom  3364  difin2  3434  symdifxor  3438  inuni  4198  eqvinop  4286  uniuni  4496  dtruex  4605  elvvv  4736  brinxp2  4740  dmuni  4886  dfres2  5008  dfima2  5021  imadmrn  5029  imai  5035  cnvxp  5098  cnvcnvsn  5156  mptpreima  5173  rnco  5186  unixpm  5215  ressn  5220  xpcom  5226  fncnv  5334  fununi  5336  imadiflem  5347  fnres  5386  fnopabg  5393  dff1o2  5521  eqfnfv3  5673  respreima  5702  fsn  5746  fliftcnv  5854  isoini  5877  spc2ed  6309  brtpos2  6327  tpostpos  6340  tposmpo  6357  nnaord  6585  pmex  6730  elpmg  6741  mapval2  6755  mapsnen  6888  map1  6889  xpsnen  6898  xpcomco  6903  elfi2  7056  supmoti  7077  cnvti  7103  2omotaplemap  7351  elni2  7409  enq0enq  7526  prltlu  7582  prnmaxl  7583  prnminu  7584  nqprrnd  7638  ltpopr  7690  letri3  8135  lesub0  8534  creur  9014  xrletri3  9908  iooneg  10092  iccneg  10093  elfzuzb  10123  fzrev  10188  redivap  11104  imdivap  11111  rersqreu  11258  lenegsq  11325  climrecvg1n  11578  fisumcom2  11668  fsumcom  11669  fprodcom2fi  11856  fprodcom  11857  gcdcom  12213  bezoutlembi  12245  dfgcd2  12254  lcmcom  12305  isprm2  12358  unennn  12687  dfrhm2  13834  issubrng  13879  ntreq0  14522  restopn2  14573  ismet2  14744  blres  14824  metrest  14896  dedekindicclemicc  15022  sincosq3sgn  15218  lgsdi  15432  lgsquadlem3  15474  2lgslem1a  15483