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 206  df-an 397

This theorem is referenced by:  ancom  461  ancom2s  647  ancom1s  650  r19.29r  3183  infsupprpr  9251  fi1uzind  14199  prmgapprmolem  16750  mat1dimcrng  21614  dmatcrng  21639  cramerlem1  21824  cramer  21828  pmatcollpwscmatlem2  21927  uhgr3cyclex  28532  3cyclfrgrrn  28636  frgrreggt1  28743  grpoidinvlem3  28854  atomli  30730  lfuhgr3  33067  cusgredgex  33069  satfun  33359  elnanelprv  33377  xpord2pred  33778  xpord3pred  33784  arg-ax  34591  bj-prmoore  35272  cnambfre  35811  prter1  36879  prjspersym  40432  mnuop3d  41848  eliuniincex  42618  eliincex  42619  dvdsn1add  43439  fourierdlem42  43649  fourierdlem80  43686  etransclem38  43772  prprelprb  44925  reupr  44930  reuopreuprim  44934  gbegt5  45169  c0snmhm  45429  pgrpgt2nabl  45658