Theorem pm3.22 460

Description: Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)

Assertion

Ref	Expression
pm3.22	⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))

Proof of Theorem pm3.22

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜑))
2	1	ancoms 459	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  ancom  461  ancom2s  656  ancom1s  659  xpord2pred  8092  infsupprpr  9416  muladdmod  13872  fi1uzind  14467  prmgapprmolem  17030  c0snmhm  20441  mat1dimcrng  22467  dmatcrng  22492  cramerlem1  22677  cramer  22681  pmatcollpwscmatlem2  22780  uhgr3cyclex  30277  3cyclfrgrrn  30381  frgrreggt1  30488  grpoidinvlem3  30602  atomli  32478  lfuhgr3  35355  cusgredgex  35357  satfun  35646  elnanelprv  35664  arg-ax  36651  bj-prmoore  37480  cnambfre  38042  prter1  39378  prjspersym  43064  rp-oelim2  43760  tfsconcatfv2  43792  tfsconcatrn  43794  oaun3lem2  43827  mnuop3d  44722  eliuniincex  45563  eliincex  45564  dvdsn1add  46389  fourierdlem42  46599  fourierdlem80  46636  etransclem38  46722  modlt0b  47839  prprelprb  47999  reupr  48004  reuopreuprim  48008  gbegt5  48259  uhgrimedg  48389  clnbgrgrim  48432  pgrpgt2nabl  48864