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  6526  tpostpos  6539  tposmpo  6556  nnaord  6786  pmex  6931  elpmg  6942  mapval2  6963  mapsnend  7103  mapsnen  7104  map1  7105  xpsnen  7123  xpcomco  7128  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  10223  iooneg  10407  iccneg  10408  elfzuzb  10439  fzrev  10508  redivap  11661  imdivap  11668  rersqreu  11816  lenegsq  11884  climrecvg1n  12139  fisumcom2  12230  fsumcom  12231  fprodcom2fi  12418  fprodcom  12419  gcdcom  12775  bezoutlembi  12807  dfgcd2  12816  lcmcom  12867  isprm2  12920  ballotfilem2  13286  unennn  13346  dfrhm2  14570  issubrng  14616  ntreq0  15358  restopn2  15409  ismet2  15580  blres  15660  metrest  15732  dedekindicclemicc  15858  sincosq3sgn  16055  bpos  16320  lgsdi  16361  lgsquadlem3  16403  2lgslem1a  16412  clwwlkn1  16864  clwwlkn2  16867  iseupthf1o  16894  eupth2lem2dc  16905  idjudju  17252  2alsraln0m  17365