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  1389  xorcom  1399  xordc  1403  xordc1  1404  dfbi3dc  1408  ancomsimp  1451  exancom  1619  19.29r  1632  19.42h  1698  19.42  1699  eu1  2067  moaneu  2118  moanmo  2119  2eu7  2136  eq2tri  2253  r19.28av  2630  r19.29r  2632  r19.42v  2651  rexcomf  2656  rabswap  2673  euxfr2dc  2946  rmo4  2954  reu8  2957  rmo3f  2958  rmo3  3078  incom  3352  difin2  3422  symdifxor  3426  inuni  4185  eqvinop  4273  uniuni  4483  dtruex  4592  elvvv  4723  brinxp2  4727  dmuni  4873  dfres2  4995  dfima2  5008  imadmrn  5016  imai  5022  cnvxp  5085  cnvcnvsn  5143  mptpreima  5160  rnco  5173  unixpm  5202  ressn  5207  xpcom  5213  fncnv  5321  fununi  5323  imadiflem  5334  fnres  5371  fnopabg  5378  dff1o2  5506  eqfnfv3  5658  respreima  5687  fsn  5731  fliftcnv  5839  isoini  5862  spc2ed  6288  brtpos2  6306  tpostpos  6319  tposmpo  6336  nnaord  6564  pmex  6709  elpmg  6720  mapval2  6734  mapsnen  6867  map1  6868  xpsnen  6877  xpcomco  6882  elfi2  7033  supmoti  7054  cnvti  7080  2omotaplemap  7319  elni2  7376  enq0enq  7493  prltlu  7549  prnmaxl  7550  prnminu  7551  nqprrnd  7605  ltpopr  7657  letri3  8102  lesub0  8500  creur  8980  xrletri3  9873  iooneg  10057  iccneg  10058  elfzuzb  10088  fzrev  10153  redivap  11021  imdivap  11028  rersqreu  11175  lenegsq  11242  climrecvg1n  11494  fisumcom2  11584  fsumcom  11585  fprodcom2fi  11772  fprodcom  11773  gcdcom  12113  bezoutlembi  12145  dfgcd2  12154  lcmcom  12205  isprm2  12258  unennn  12557  dfrhm2  13653  issubrng  13698  ntreq0  14311  restopn2  14362  ismet2  14533  blres  14613  metrest  14685  dedekindicclemicc  14811  sincosq3sgn  15004  lgsdi  15194  lgsquadlem3  15236  2lgslem1a  15245