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  8097  infsupprpr  9421  muladdmod  13847  fi1uzind  14442  prmgapprmolem  17001  c0snmhm  20411  mat1dimcrng  22433  dmatcrng  22458  cramerlem1  22643  cramer  22647  pmatcollpwscmatlem2  22746  uhgr3cyclex  30269  3cyclfrgrrn  30373  frgrreggt1  30480  grpoidinvlem3  30593  atomli  32469  lfuhgr3  35333  cusgredgex  35335  satfun  35624  elnanelprv  35642  arg-ax  36629  bj-prmoore  37362  cnambfre  37913  prter1  39249  prjspersym  42959  rp-oelim2  43659  tfsconcatfv2  43691  tfsconcatrn  43693  oaun3lem2  43726  mnuop3d  44621  eliuniincex  45462  eliincex  45463  dvdsn1add  46291  fourierdlem42  46501  fourierdlem80  46538  etransclem38  46624  modlt0b  47717  prprelprb  47871  reupr  47876  reuopreuprim  47880  gbegt5  48115  uhgrimedg  48245  clnbgrgrim  48288  pgrpgt2nabl  48720