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

This theorem is referenced by:  ancom  460  ancom2s  649  ancom1s  652  r19.29rOLD  3112  xpord2pred  8144  infsupprpr  9521  fi1uzind  14484  prmgapprmolem  17023  c0snmhm  20395  mat1dimcrng  22372  dmatcrng  22397  cramerlem1  22582  cramer  22586  pmatcollpwscmatlem2  22685  uhgr3cyclex  29985  3cyclfrgrrn  30089  frgrreggt1  30196  grpoidinvlem3  30309  atomli  32185  lfuhgr3  34719  cusgredgex  34721  satfun  35011  elnanelprv  35029  arg-ax  35890  bj-prmoore  36584  cnambfre  37130  prter1  38340  prjspersym  42003  rp-oelim2  42709  tfsconcatfv2  42741  tfsconcatrn  42743  oaun3lem2  42776  mnuop3d  43680  eliuniincex  44447  eliincex  44448  dvdsn1add  45299  fourierdlem42  45509  fourierdlem80  45546  etransclem38  45632  prprelprb  46829  reupr  46834  reuopreuprim  46838  gbegt5  47073  pgrpgt2nabl  47402