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  824  rbaib  926  rbaibr  927  ifptru  995  ifpfal  996  3anrot  1007  3ancoma  1009  excxor  1420  xorcom  1430  xordc  1434  xordc1  1435  dfbi3dc  1439  ancomsimp  1483  exancom  1654  19.29r  1667  19.42h  1733  19.42  1734  eu1  2102  moaneu  2154  moanmo  2155  2eu7  2172  eq2tri  2289  r19.28av  2667  r19.29r  2669  r19.42v  2688  rexcomf  2693  rabswap  2710  euxfr2dc  2989  rmo4  2997  reu8  3000  rmo3f  3001  rmo3  3122  incom  3397  difin2  3467  symdifxor  3471  elif  3615  inuni  4243  eqvinop  4333  uniuni  4546  dtruex  4655  elvvv  4787  brinxp2  4791  dmuni  4939  dfres2  5063  dfima2  5076  imadmrn  5084  imai  5090  cnvxp  5153  cnvcnvsn  5211  mptpreima  5228  rnco  5241  unixpm  5270  ressn  5275  xpcom  5281  fncnv  5393  fununi  5395  imadiflem  5406  fnres  5446  fnopabg  5453  dff1o2  5585  eqfnfv3  5742  respreima  5771  fsn  5815  fliftcnv  5931  isoini  5954  spc2ed  6393  brtpos2  6412  tpostpos  6425  tposmpo  6442  nnaord  6672  pmex  6817  elpmg  6828  mapval2  6842  mapsnen  6981  map1  6982  xpsnen  7000  xpcomco  7005  elfi2  7162  supmoti  7183  cnvti  7209  2omotaplemap  7466  elni2  7524  enq0enq  7641  prltlu  7697  prnmaxl  7698  prnminu  7699  nqprrnd  7753  ltpopr  7805  letri3  8250  lesub0  8649  creur  9129  xrletri3  10029  iooneg  10213  iccneg  10214  elfzuzb  10244  fzrev  10309  redivap  11425  imdivap  11432  rersqreu  11579  lenegsq  11646  climrecvg1n  11899  fisumcom2  11989  fsumcom  11990  fprodcom2fi  12177  fprodcom  12178  gcdcom  12534  bezoutlembi  12566  dfgcd2  12575  lcmcom  12626  isprm2  12679  unennn  13008  dfrhm2  14158  issubrng  14203  ntreq0  14846  restopn2  14897  ismet2  15068  blres  15148  metrest  15220  dedekindicclemicc  15346  sincosq3sgn  15542  lgsdi  15756  lgsquadlem3  15798  2lgslem1a  15807  clwwlkn1  16213  clwwlkn2  16216  iseupthf1o  16243