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  646  ancom1s  649  r19.29r  3184  infsupprpr  9193  fi1uzind  14139  prmgapprmolem  16690  mat1dimcrng  21534  dmatcrng  21559  cramerlem1  21744  cramer  21748  pmatcollpwscmatlem2  21847  uhgr3cyclex  28447  3cyclfrgrrn  28551  frgrreggt1  28658  grpoidinvlem3  28769  atomli  30645  lfuhgr3  32981  cusgredgex  32983  satfun  33273  elnanelprv  33291  xpord2pred  33719  xpord3pred  33725  arg-ax  34532  bj-prmoore  35213  cnambfre  35752  prter1  36820  prjspersym  40367  mnuop3d  41778  eliuniincex  42548  eliincex  42549  dvdsn1add  43370  fourierdlem42  43580  fourierdlem80  43617  etransclem38  43703  prprelprb  44857  reupr  44862  reuopreuprim  44866  gbegt5  45101  c0snmhm  45361  pgrpgt2nabl  45590