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  731  rbaib  829  rbaibr  830  3anrot  889  3ancoma  891  excxor  1268  xorcom  1276  xordc  1280  xordc1  1281  dfbi3dc  1285  ancomsimp  1326  exancom  1496  19.29r  1509  19.42h  1574  19.42  1575  eu1  1922  moaneu  1973  moanmo  1974  2eu7  1991  eq2tri  2096  r19.28av  2443  r19.29r  2445  r19.42v  2461  rexcomf  2466  rabswap  2482  euxfr2dc  2720  rmo4  2728  reu8  2731  rmo3  2843  incom  3123  difin2  3193  symdifxor  3197  inuni  3900  eqvinop  3971  uniuni  4149  dtruex  4237  elvvv  4346  brinxp2  4350  dmuni  4488  dfres2  4601  dfima2  4613  imadmrn  4621  imai  4624  cnvxp  4685  cnvcnvsn  4740  mptpreima  4757  rnco  4770  unixpm  4796  ressn  4801  xpcom  4807  fncnv  4908  fununi  4910  imadiflem  4921  fnres  4958  fnopabg  4965  dff1o2  5074  eqfnfv3  5210  respreima  5238  fsn  5278  fliftcnv  5378  isoini  5400  brtpos2  5807  tpostpos  5820  tposmpt2  5837  nnaord  6018  xpsnen  6231  xpcomco  6236  elni2  6298  enq0enq  6413  prltlu  6469  prnmaxl  6470  prnminu  6471  nqprrnd  6526  ltpopr  6567  letri3  6856  lesub0  7229  creur  7652  xrletri3  8451  iooneg  8586  iccneg  8587  elfzuzb  8614  fzrev  8676  redivap  9062  imdivap  9069