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 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
StepHypRef Expression
1 id 22 . 2 ((𝜓𝜑) → (𝜓𝜑))
21ancoms 462 1 ((𝜑𝜓) → (𝜓𝜑))
Colors of variables: wff setvar class
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 210  df-an 400
This theorem is referenced by:  ancom  464  ancom2s  649  ancom1s  652  r19.29r  3217  infsupprpr  8952  fi1uzind  13851  prmgapprmolem  16387  mat1dimcrng  21082  dmatcrng  21107  cramerlem1  21292  cramer  21296  pmatcollpwscmatlem2  21395  uhgr3cyclex  27967  3cyclfrgrrn  28071  frgrreggt1  28178  grpoidinvlem3  28289  atomli  30165  lfuhgr3  32479  cusgredgex  32481  satfun  32771  elnanelprv  32789  arg-ax  33877  bj-prmoore  34530  cnambfre  35105  prter1  36175  prjspersym  39599  mnuop3d  40977  eliuniincex  41743  eliincex  41744  dvdsn1add  42579  fourierdlem42  42789  fourierdlem80  42826  etransclem38  42912  prprelprb  44032  reupr  44037  reuopreuprim  44041  gbegt5  44277  c0snmhm  44537  pgrpgt2nabl  44766
  Copyright terms: Public domain W3C validator