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  3356  difin2  3426  symdifxor  3430  inuni  4189  eqvinop  4277  uniuni  4487  dtruex  4596  elvvv  4727  brinxp2  4731  dmuni  4877  dfres2  4999  dfima2  5012  imadmrn  5020  imai  5026  cnvxp  5089  cnvcnvsn  5147  mptpreima  5164  rnco  5177  unixpm  5206  ressn  5211  xpcom  5217  fncnv  5325  fununi  5327  imadiflem  5338  fnres  5377  fnopabg  5384  dff1o2  5512  eqfnfv3  5664  respreima  5693  fsn  5737  fliftcnv  5845  isoini  5868  spc2ed  6300  brtpos2  6318  tpostpos  6331  tposmpo  6348  nnaord  6576  pmex  6721  elpmg  6732  mapval2  6746  mapsnen  6879  map1  6880  xpsnen  6889  xpcomco  6894  elfi2  7047  supmoti  7068  cnvti  7094  2omotaplemap  7342  elni2  7400  enq0enq  7517  prltlu  7573  prnmaxl  7574  prnminu  7575  nqprrnd  7629  ltpopr  7681  letri3  8126  lesub0  8525  creur  9005  xrletri3  9898  iooneg  10082  iccneg  10083  elfzuzb  10113  fzrev  10178  redivap  11058  imdivap  11065  rersqreu  11212  lenegsq  11279  climrecvg1n  11532  fisumcom2  11622  fsumcom  11623  fprodcom2fi  11810  fprodcom  11811  gcdcom  12167  bezoutlembi  12199  dfgcd2  12208  lcmcom  12259  isprm2  12312  unennn  12641  dfrhm2  13788  issubrng  13833  ntreq0  14476  restopn2  14527  ismet2  14698  blres  14778  metrest  14850  dedekindicclemicc  14976  sincosq3sgn  15172  lgsdi  15386  lgsquadlem3  15428  2lgslem1a  15437