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  8086  infsupprpr  9410  muladdmod  13863  fi1uzind  14458  prmgapprmolem  17021  c0snmhm  20432  mat1dimcrng  22451  dmatcrng  22476  cramerlem1  22661  cramer  22665  pmatcollpwscmatlem2  22764  uhgr3cyclex  30272  3cyclfrgrrn  30376  frgrreggt1  30483  grpoidinvlem3  30597  atomli  32473  lfuhgr3  35323  cusgredgex  35325  satfun  35614  elnanelprv  35632  arg-ax  36619  bj-prmoore  37440  cnambfre  38000  prter1  39336  prjspersym  43051  rp-oelim2  43751  tfsconcatfv2  43783  tfsconcatrn  43785  oaun3lem2  43818  mnuop3d  44713  eliuniincex  45554  eliincex  45555  dvdsn1add  46382  fourierdlem42  46592  fourierdlem80  46629  etransclem38  46715  modlt0b  47814  prprelprb  47974  reupr  47979  reuopreuprim  47983  gbegt5  48234  uhgrimedg  48364  clnbgrgrim  48407  pgrpgt2nabl  48839