MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm3.22 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 id 22 . 2 ((𝜓𝜑) → (𝜓𝜑))
21ancoms 458 1 ((𝜑𝜓) → (𝜓𝜑))
Colors of variables: wff setvar class
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  650  ancom1s  653  r19.29rOLD  3116  xpord2pred  8171  infsupprpr  9545  muladdmod  13954  fi1uzind  14547  prmgapprmolem  17100  c0snmhm  20464  mat1dimcrng  22484  dmatcrng  22509  cramerlem1  22694  cramer  22698  pmatcollpwscmatlem2  22797  uhgr3cyclex  30202  3cyclfrgrrn  30306  frgrreggt1  30413  grpoidinvlem3  30526  atomli  32402  lfuhgr3  35126  cusgredgex  35128  satfun  35417  elnanelprv  35435  arg-ax  36418  bj-prmoore  37117  cnambfre  37676  prter1  38881  prjspersym  42622  rp-oelim2  43326  tfsconcatfv2  43358  tfsconcatrn  43360  oaun3lem2  43393  mnuop3d  44295  eliuniincex  45119  eliincex  45120  dvdsn1add  45959  fourierdlem42  46169  fourierdlem80  46206  etransclem38  46292  prprelprb  47509  reupr  47514  reuopreuprim  47518  gbegt5  47753  clnbgrgrim  47907  pgrpgt2nabl  48287
  Copyright terms: Public domain W3C validator