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  651  ancom1s  654  xpord2pred  8095  infsupprpr  9419  muladdmod  13874  fi1uzind  14469  prmgapprmolem  17032  c0snmhm  20443  mat1dimcrng  22442  dmatcrng  22467  cramerlem1  22652  cramer  22656  pmatcollpwscmatlem2  22755  uhgr3cyclex  30252  3cyclfrgrrn  30356  frgrreggt1  30463  grpoidinvlem3  30577  atomli  32453  lfuhgr3  35302  cusgredgex  35304  satfun  35593  elnanelprv  35611  arg-ax  36598  bj-prmoore  37427  cnambfre  37989  prter1  39325  prjspersym  43040  rp-oelim2  43736  tfsconcatfv2  43768  tfsconcatrn  43770  oaun3lem2  43803  mnuop3d  44698  eliuniincex  45539  eliincex  45540  dvdsn1add  46367  fourierdlem42  46577  fourierdlem80  46614  etransclem38  46700  modlt0b  47817  prprelprb  47977  reupr  47982  reuopreuprim  47986  gbegt5  48237  uhgrimedg  48367  clnbgrgrim  48410  pgrpgt2nabl  48842