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  480  an32  481  an13  482  an42  506  andir  716  rbaib  814  rbaibr  815  3anrot  874  3ancoma  876  excxor  1252  xorcom  1260  xordc  1264  xordc1  1265  dfbi3dc  1269  ancomsimp  1305  exancom  1475  19.29r  1488  19.42h  1553  19.42  1554  eu1  1901  moaneu  1952  moanmo  1953  2eu7  1970  eq2tri  2075  r19.28av  2421  r19.29r  2423  r19.42v  2439  rexcomf  2444  rabswap  2460  euxfr2dc  2697  rmo4  2705  reu8  2708  rmo3  2820  incom  3100  difin2  3170  symdifxor  3174  inuni  3875  eqvinop  3946  uniuni  4124  dtruex  4212  elvvv  4321  brinxp2  4325  dmuni  4463  dfres2  4576  dfima2  4588  imadmrn  4596  imai  4599  cnvxp  4660  cnvcnvsn  4715  mptpreima  4732  rnco  4745  unixpm  4771  ressn  4776  xpcom  4782  fncnv  4882  fununi  4884  imadiflem  4895  fnres  4932  fnopabg  4939  dff1o2  5047  eqfnfv3  5183  respreima  5211  fsn  5251  fliftcnv  5351  isoini  5373  brtpos2  5779  tpostpos  5792  tposmpt2  5809  nnaord  5984  elni2  6163  enq0enq  6275  prltlu  6330  prnmaxl  6331  prnminu  6332  nqprrnd  6387  ltpopr  6421  letri3  6702  lesub0  7075  creur  7497  xrletri3  8200  iooneg  8335  iccneg  8336