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 447
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 446 1 ((𝜑𝜓) → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 197  df-an 383
This theorem is referenced by:  ancom  448  ancom2s  629  ancom1s  632  fi1uzind  13481  cshwlen  13754  prmgapprmolem  15972  setsstructOLD  16106  mat1dimcrng  20501  dmatcrng  20526  cramerlem1  20713  cramer  20717  pmatcollpwscmatlem2  20815  uhgr3cyclex  27362  3cyclfrgrrn  27468  frgrreggt1  27592  grpoidinvlem3  27700  atomli  29581  arg-ax  32752  cnambfre  33789  prter1  34685  eliuniincex  39811  eliincex  39812  dvdsn1add  40667  fourierdlem42  40878  fourierdlem80  40915  etransclem38  41001  gbegt5  42172  c0snmhm  42438  pgrpgt2nabl  42670
  Copyright terms: Public domain W3C validator