Theorem pm3.22 459

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 458	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ancom  460  ancom2s  650  ancom1s  653  xpord2pred  8085  infsupprpr  9415  muladdmod  13837  fi1uzind  14432  prmgapprmolem  16991  c0snmhm  20366  mat1dimcrng  22380  dmatcrng  22405  cramerlem1  22590  cramer  22594  pmatcollpwscmatlem2  22693  uhgr3cyclex  30144  3cyclfrgrrn  30248  frgrreggt1  30355  grpoidinvlem3  30468  atomli  32344  lfuhgr3  35092  cusgredgex  35094  satfun  35383  elnanelprv  35401  arg-ax  36389  bj-prmoore  37088  cnambfre  37647  prter1  38857  prjspersym  42580  rp-oelim2  43281  tfsconcatfv2  43313  tfsconcatrn  43315  oaun3lem2  43348  mnuop3d  44244  eliuniincex  45087  eliincex  45088  dvdsn1add  45921  fourierdlem42  46131  fourierdlem80  46168  etransclem38  46254  modlt0b  47348  prprelprb  47502  reupr  47507  reuopreuprim  47511  gbegt5  47746  uhgrimedg  47876  clnbgrgrim  47919  pgrpgt2nabl  48351