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  1622  19.29r  1635  19.42h  1701  19.42  1702  eu1  2070  moaneu  2121  moanmo  2122  2eu7  2139  eq2tri  2256  r19.28av  2633  r19.29r  2635  r19.42v  2654  rexcomf  2659  rabswap  2676  euxfr2dc  2949  rmo4  2957  reu8  2960  rmo3f  2961  rmo3  3081  incom  3355  difin2  3425  symdifxor  3429  inuni  4188  eqvinop  4276  uniuni  4486  dtruex  4595  elvvv  4726  brinxp2  4730  dmuni  4876  dfres2  4998  dfima2  5011  imadmrn  5019  imai  5025  cnvxp  5088  cnvcnvsn  5146  mptpreima  5163  rnco  5176  unixpm  5205  ressn  5210  xpcom  5216  fncnv  5324  fununi  5326  imadiflem  5337  fnres  5374  fnopabg  5381  dff1o2  5509  eqfnfv3  5661  respreima  5690  fsn  5734  fliftcnv  5842  isoini  5865  spc2ed  6291  brtpos2  6309  tpostpos  6322  tposmpo  6339  nnaord  6567  pmex  6712  elpmg  6723  mapval2  6737  mapsnen  6870  map1  6871  xpsnen  6880  xpcomco  6885  elfi2  7038  supmoti  7059  cnvti  7085  2omotaplemap  7324  elni2  7381  enq0enq  7498  prltlu  7554  prnmaxl  7555  prnminu  7556  nqprrnd  7610  ltpopr  7662  letri3  8107  lesub0  8506  creur  8986  xrletri3  9879  iooneg  10063  iccneg  10064  elfzuzb  10094  fzrev  10159  redivap  11039  imdivap  11046  rersqreu  11193  lenegsq  11260  climrecvg1n  11513  fisumcom2  11603  fsumcom  11604  fprodcom2fi  11791  fprodcom  11792  gcdcom  12140  bezoutlembi  12172  dfgcd2  12181  lcmcom  12232  isprm2  12285  unennn  12614  dfrhm2  13710  issubrng  13755  ntreq0  14368  restopn2  14419  ismet2  14590  blres  14670  metrest  14742  dedekindicclemicc  14868  sincosq3sgn  15064  lgsdi  15278  lgsquadlem3  15320  2lgslem1a  15329