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 2206
Description: Inference form of 19.21 2222 and also deduction form of sp 2200. (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 2200 . 2 (∀𝑥𝜓𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196
This theorem depends on definitions:  df-bi 197  df-ex 1854
This theorem is referenced by:  19.21bbi  2207  eqeq1dALT  2763  eleq2dALT  2826  ssel  3738  pocl  5194  funmo  6065  funun  6093  fununi  6125  findcard  8366  findcard2  8367  axpowndlem4  9634  axregndlem2  9637  axinfnd  9640  prcdnq  10027  dfrtrcl2  14021  relexpindlem  14022  bnj1379  31229  bnj1052  31371  bnj1118  31380  bnj1154  31395  bnj1280  31416  dftrcl3  38532  dfrtrcl3  38545  vk15.4j  39254  hbimpg  39290
  Copyright terms: Public domain W3C validator