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

Theorem pm3.22 465
 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 pm3.21 464 . 2 (𝜑 → (𝜓 → (𝜓𝜑)))
21imp 445 1 ((𝜑𝜓) → (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 386 This theorem is referenced by:  ancom  466  ancom2s  843  ancom1s  846  fi1uzind  13218  fi1uzindOLD  13224  cshwlen  13482  prmgapprmolem  15689  setsstructOLD  15820  mat1dimcrng  20202  dmatcrng  20227  cramerlem1  20412  cramer  20416  pmatcollpwscmatlem2  20514  uhgr3cyclex  26908  3cyclfrgrrn  27014  frgrreggt1  27105  grpoidinvlem3  27206  atomli  29087  arg-ax  32054  cnambfre  33087  prter1  33641  eliuniincex  38776  eliincex  38777  dvdsn1add  39457  fourierdlem42  39670  fourierdlem80  39707  etransclem38  39793  gbegt5  40941  c0snmhm  41200  pgrpgt2nabl  41432
 Copyright terms: Public domain W3C validator