Theorem pm3.22 463

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 462	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ancom  464  ancom2s  660  ancom1s  663  xpord2pred  8120  infsupprpr  9449  muladdmod  13922  fi1uzind  14517  prmgapprmolem  17080  c0snmhm  20491  mat1dimcrng  22517  dmatcrng  22542  cramerlem1  22727  cramer  22731  pmatcollpwscmatlem2  22830  uhgr3cyclex  30330  3cyclfrgrrn  30434  frgrreggt1  30541  grpoidinvlem3  30655  atomli  32531  lfuhgr3  35434  cusgredgex  35436  satfun  35725  elnanelprv  35743  arg-ax  36740  bj-prmoore  37569  cnambfre  38131  prter1  39467  prjspersym  43153  rp-oelim2  43849  tfsconcatfv2  43881  tfsconcatrn  43883  oaun3lem2  43916  mnuop3d  44811  eliuniincex  45651  eliincex  45652  dvdsn1add  46477  fourierdlem42  46687  fourierdlem80  46724  etransclem38  46810  modlt0b  47927  prprelprb  48087  reupr  48092  reuopreuprim  48096  gbegt5  48347  uhgrimedg  48477  clnbgrgrim  48520  pgrpgt2nabl  48952