Theorem ancom 253

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 252	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))
2		pm3.22 252	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓))
3	1, 2	impbii 117	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ancomd  254  ancomsd  256  pm4.71r  370  pm5.32rd  424  pm5.32ri  428  anbi2ci  432  anbi12ci  434  mpan10  443  an12  495  an32  496  an13  497  an42  521  andir  732  rbaib  830  rbaibr  831  3anrot  890  3ancoma  892  excxor  1269  xorcom  1279  xordc  1283  xordc1  1284  dfbi3dc  1288  ancomsimp  1329  exancom  1499  19.29r  1512  19.42h  1577  19.42  1578  eu1  1925  moaneu  1976  moanmo  1977  2eu7  1994  eq2tri  2099  r19.28av  2449  r19.29r  2451  r19.42v  2467  rexcomf  2472  rabswap  2488  euxfr2dc  2726  rmo4  2734  reu8  2737  rmo3  2849  incom  3129  difin2  3199  symdifxor  3203  inuni  3909  eqvinop  3980  uniuni  4183  dtruex  4283  elvvv  4403  brinxp2  4407  dmuni  4545  dfres2  4658  dfima2  4670  imadmrn  4678  imai  4681  cnvxp  4742  cnvcnvsn  4797  mptpreima  4814  rnco  4827  unixpm  4853  ressn  4858  xpcom  4864  fncnv  4965  fununi  4967  imadiflem  4978  fnres  5015  fnopabg  5022  dff1o2  5131  eqfnfv3  5267  respreima  5295  fsn  5335  fliftcnv  5435  isoini  5457  brtpos2  5866  tpostpos  5879  tposmpt2  5896  nnaord  6082  xpsnen  6295  xpcomco  6300  elni2  6412  enq0enq  6529  prltlu  6585  prnmaxl  6586  prnminu  6587  nqprrnd  6641  ltpopr  6693  letri3  7099  lesub0  7474  creur  7911  xrletri3  8721  iooneg  8856  iccneg  8857  elfzuzb  8884  fzrev  8946  redivap  9474  imdivap  9481  rersqreu  9626  lenegsq  9691  climrecvg1n  9867