Theorem ancom 262

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 261	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))
2		pm3.22 261	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓))
3	1, 2	impbii 124	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ∧ wa 102   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ancomd  263  ancomsd  265  pm4.71r  382  pm5.32rd  438  pm5.32ri  442  anbi2ci  446  anbi12ci  448  mpan10  457  an12  525  an32  526  an13  527  an42  551  andir  765  rbaib  863  rbaibr  864  3anrot  924  3ancoma  926  excxor  1309  xorcom  1319  xordc  1323  xordc1  1324  dfbi3dc  1328  ancomsimp  1369  exancom  1539  19.29r  1552  19.42h  1617  19.42  1618  eu1  1966  moaneu  2017  moanmo  2018  2eu7  2035  eq2tri  2140  r19.28av  2493  r19.29r  2495  r19.42v  2511  rexcomf  2516  rabswap  2532  euxfr2dc  2777  rmo4  2785  reu8  2788  rmo3  2905  incom  3158  difin2  3226  symdifxor  3230  inuni  3930  eqvinop  3998  uniuni  4201  dtruex  4302  elvvv  4421  brinxp2  4425  dmuni  4563  dfres2  4678  dfima2  4690  imadmrn  4698  imai  4701  cnvxp  4762  cnvcnvsn  4817  mptpreima  4834  rnco  4847  unixpm  4873  ressn  4878  xpcom  4884  fncnv  4985  fununi  4987  imadiflem  4998  fnres  5035  fnopabg  5042  dff1o2  5151  eqfnfv3  5288  respreima  5316  fsn  5356  fliftcnv  5455  isoini  5477  spc2ed  5874  brtpos2  5889  tpostpos  5902  tposmpt2  5919  nnaord  6105  xpsnen  6318  xpcomco  6323  supmoti  6406  cnvti  6432  elni2  6504  enq0enq  6621  prltlu  6677  prnmaxl  6678  prnminu  6679  nqprrnd  6733  ltpopr  6785  letri3  7192  lesub0  7583  creur  8036  xrletri3  8875  iooneg  9010  iccneg  9011  elfzuzb  9039  fzrev  9101  redivap  9761  imdivap  9768  rersqreu  9914  lenegsq  9981  climrecvg1n  10185  gcdcom  10365  bezoutlembi  10394  dfgcd2  10403  lcmcom  10446  isprm2  10499