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 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ancomd  267  ancomsd  269  biancomi  270  biancomd  271  pm4.71r  394  pm5.32rd  455  pm5.32ri  459  anbi2ci  463  anbi12ci  465  bianassc  474  mpan10  478  an12  567  an32  568  an13  569  an42  593  andir  831  rbaib  933  rbaibr  934  ifptru  1002  ifpfal  1003  3anrot  1014  3ancoma  1016  excxor  1427  xorcom  1437  xordc  1441  xordc1  1442  dfbi3dc  1446  ancomsimp  1490  exancom  1661  19.29r  1674  19.42h  1739  19.42  1740  eu1  2111  moaneu  2163  moanmo  2164  2eu7  2181  eq2tri  2298  r19.28av  2687  r19.29r  2689  r19.42v  2708  rexcomf  2713  rabswap  2731  euxfr2dc  3011  rmo4  3019  reu8  3022  rmo3f  3023  rmo3  3144  incom  3421  difin2  3493  symdifxor  3497  elif  3652  inuni  4293  eqvinop  4385  uniuni  4599  dtruex  4708  elvvv  4840  brinxp2  4844  dmuni  4993  dfres2  5118  dfima2  5131  imadmrn  5139  imai  5146  cnvxp  5209  cnvcnvsn  5267  mptpreima  5284  rnco  5297  unixpm  5326  ressn  5331  xpcom  5337  fncnv  5450  fununi  5452  imadiflem  5463  fnres  5503  fnopabg  5510  dff1o2  5647  eqfnfv3  5811  respreima  5839  fsn  5883  fliftcnv  6004  isoini  6027  spc2ed  6473  brtpos2  6527  tpostpos  6540  tposmpo  6557  nnaord  6787  pmex  6932  elpmg  6943  mapval2  6964  mapsnend  7105  mapsnen  7106  map1  7107  xpsnen  7125  xpcomco  7130  elfi2  7311  supmoti  7339  cnvti  7365  2omotaplemap  7629  elni2  7687  enq0enq  7804  prltlu  7860  prnmaxl  7861  prnminu  7862  nqprrnd  7916  ltpopr  7968  letri3  8412  lesub0  8814  creur  9297  xrletri3  10222  iooneg  10406  iccneg  10407  elfzuzb  10438  fzrev  10507  redivap  11660  imdivap  11667  rersqreu  11815  lenegsq  11883  climrecvg1n  12138  fisumcom2  12229  fsumcom  12230  fprodcom2fi  12417  fprodcom  12418  gcdcom  12774  bezoutlembi  12806  dfgcd2  12815  lcmcom  12866  isprm2  12919  ballotfilem2  13285  unennn  13345  dfrhm2  14569  issubrng  14615  ntreq0  15375  restopn2  15426  ismet2  15597  blres  15677  metrest  15749  dedekindicclemicc  15875  sincosq3sgn  16072  bpos  16337  lgsdi  16378  lgsquadlem3  16420  2lgslem1a  16429  clwwlkn1  16881  clwwlkn2  16884  iseupthf1o  16911  eupth2lem2dc  16922  idjudju  17269  2alsraln0m  17382