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  4497  dtruex  4606  elvvv  4737  brinxp2  4741  dmuni  4887  dfres2  5010  dfima2  5023  imadmrn  5031  imai  5037  cnvxp  5100  cnvcnvsn  5158  mptpreima  5175  rnco  5188  unixpm  5217  ressn  5222  xpcom  5228  fncnv  5339  fununi  5341  imadiflem  5352  fnres  5391  fnopabg  5398  dff1o2  5526  eqfnfv3  5678  respreima  5707  fsn  5751  fliftcnv  5863  isoini  5886  spc2ed  6318  brtpos2  6336  tpostpos  6349  tposmpo  6366  nnaord  6594  pmex  6739  elpmg  6750  mapval2  6764  mapsnen  6902  map1  6903  xpsnen  6915  xpcomco  6920  elfi2  7073  supmoti  7094  cnvti  7120  2omotaplemap  7368  elni2  7426  enq0enq  7543  prltlu  7599  prnmaxl  7600  prnminu  7601  nqprrnd  7655  ltpopr  7707  letri3  8152  lesub0  8551  creur  9031  xrletri3  9925  iooneg  10109  iccneg  10110  elfzuzb  10140  fzrev  10205  redivap  11127  imdivap  11134  rersqreu  11281  lenegsq  11348  climrecvg1n  11601  fisumcom2  11691  fsumcom  11692  fprodcom2fi  11879  fprodcom  11880  gcdcom  12236  bezoutlembi  12268  dfgcd2  12277  lcmcom  12328  isprm2  12381  unennn  12710  dfrhm2  13858  issubrng  13903  ntreq0  14546  restopn2  14597  ismet2  14768  blres  14848  metrest  14920  dedekindicclemicc  15046  sincosq3sgn  15242  lgsdi  15456  lgsquadlem3  15498  2lgslem1a  15507