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 460
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 459 1 ((𝜑𝜓) → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  ancom  461  ancom2s  646  ancom1s  649  r19.29r  3255  infsupprpr  8957  fi1uzind  13845  prmgapprmolem  16387  mat1dimcrng  21016  dmatcrng  21041  cramerlem1  21226  cramer  21230  pmatcollpwscmatlem2  21328  uhgr3cyclex  27889  3cyclfrgrrn  27993  frgrreggt1  28100  grpoidinvlem3  28211  atomli  30087  lfuhgr3  32264  cusgredgex  32266  satfun  32556  elnanelprv  32574  arg-ax  33662  cnambfre  34822  prter1  35897  prjspersym  39137  mnuop3d  40487  eliuniincex  41256  eliincex  41257  dvdsn1add  42104  fourierdlem42  42315  fourierdlem80  42352  etransclem38  42438  prprelprb  43526  reupr  43531  reuopreuprim  43535  gbegt5  43773  c0snmhm  44084  pgrpgt2nabl  44312
  Copyright terms: Public domain W3C validator