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  r19.29rOLD  3115  xpord2pred  8169  infsupprpr  9542  muladdmod  13950  fi1uzind  14543  prmgapprmolem  17095  c0snmhm  20480  mat1dimcrng  22499  dmatcrng  22524  cramerlem1  22709  cramer  22713  pmatcollpwscmatlem2  22812  uhgr3cyclex  30211  3cyclfrgrrn  30315  frgrreggt1  30422  grpoidinvlem3  30535  atomli  32411  lfuhgr3  35104  cusgredgex  35106  satfun  35396  elnanelprv  35414  arg-ax  36399  bj-prmoore  37098  cnambfre  37655  prter1  38861  prjspersym  42594  rp-oelim2  43298  tfsconcatfv2  43330  tfsconcatrn  43332  oaun3lem2  43365  mnuop3d  44267  eliuniincex  45049  eliincex  45050  dvdsn1add  45895  fourierdlem42  46105  fourierdlem80  46142  etransclem38  46228  prprelprb  47442  reupr  47447  reuopreuprim  47451  gbegt5  47686  clnbgrgrim  47840  pgrpgt2nabl  48211