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

Theorem 19.21bi 2213
Description: Inference form of 19.21 2231 and also deduction form of sp 2207. (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
19.21bi.1 (𝜑 → ∀𝑥𝜓)
Assertion
Ref Expression
19.21bi (𝜑𝜓)

Proof of Theorem 19.21bi
StepHypRef Expression
1 19.21bi.1 . 2 (𝜑 → ∀𝑥𝜓)
2 sp 2207 . 2 (∀𝑥𝜓𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203
This theorem depends on definitions:  df-bi 197  df-ex 1853
This theorem is referenced by:  19.21bbi  2214  axc7e  2297  eqeq1dALT  2774  eleq2dALT  2837  ssel  3746  pocl  5177  funmo  6047  funun  6075  fununi  6104  findcard  8355  findcard2  8356  axpowndlem4  9624  axregndlem2  9627  axinfnd  9630  prcdnq  10017  dfrtrcl2  14010  relexpindlem  14011  bnj1379  31239  bnj1052  31381  bnj1118  31390  bnj1154  31405  bnj1280  31426  dftrcl3  38538  dfrtrcl3  38551  vk15.4j  39259  hbimpg  39295
  Copyright terms: Public domain W3C validator