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

Theorem pm2.27 42
Description: This theorem, called "Assertion," can be thought of as closed form of modus ponens ax-mp 5. Theorem *2.27 of [WhiteheadRussell] p. 104. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
pm2.27 (𝜑 → ((𝜑𝜓) → 𝜓))

Proof of Theorem pm2.27
StepHypRef Expression
1 id 22 . 2 ((𝜑𝜓) → (𝜑𝜓))
21com12 32 1 (𝜑 → ((𝜑𝜓) → 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  pm2.43  56  com23  86  pm3.2im  157  mth8  158  biimt  350  pm3.35  610  pm2.26  926  cases2  992  19.35  1802  axc16g  2130  axc11rvOLD  2136  axc11r  2186  issref  5478  fundif  5903  tfinds  7021  tfindsg  7022  smogt  7424  findcard2  8160  findcard3  8163  fisupg  8168  xpfi  8191  dffi2  8289  fiinfg  8365  cantnfle  8528  ac5num  8819  pwsdompw  8986  cfsmolem  9052  axcc4  9221  axdc3lem2  9233  fpwwe2lem8  9419  pwfseqlem3  9442  tskord  9562  grudomon  9599  grur1a  9601  xrub  12101  relexprelg  13728  coprmproddvdslem  15319  pcmptcl  15538  restntr  20926  cmpsublem  21142  cmpsub  21143  txlm  21391  ptcmplem3  21798  c1lip1  23698  wilthlem3  24730  dmdbr5  29055  wzel  31525  wzelOLD  31526  waj-ax  32108  lukshef-ax2  32109  bj-axd2d  32272  bj-sbex  32321  bj-ssbeq  32322  bj-ssb0  32323  bj-eqs  32358  bj-sbsb  32520  finixpnum  33065  mbfresfi  33127  filbcmb  33206  orfa  33552  axc11n-16  33742  axc11-o  33755  axc5c4c711toc7  38126  axc5c4c711to11  38127  ax6e2nd  38295  elex22VD  38596  exbiriVD  38611  ssralv2VD  38624  truniALTVD  38636  trintALTVD  38638  onfrALTVD  38649  hbimpgVD  38662  ax6e2eqVD  38665  ax6e2ndVD  38666  fmtnofac2lem  40809  bgoldbwt  40990  bgoldbst  40991  nnsum4primesodd  41003  nnsum4primesoddALTV  41004  bgoldbnnsum3prm  41011  tgoldbach  41023  tgoldbachOLD  41030  snlindsntor  41578
  Copyright terms: Public domain W3C validator