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 2057
Description: Inference form of 19.21 2073 and also deduction form of sp 2051. (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 2051 . 2 (∀𝑥𝜓𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045
This theorem depends on definitions:  df-bi 197  df-ex 1703
This theorem is referenced by:  19.21bbi  2058  eqeq1dALT  2623  eleq2dALT  2686  ssel  3589  pocl  5032  funmo  5892  funun  5920  fununi  5952  findcard  8184  findcard2  8185  axpowndlem4  9407  axregndlem2  9410  axinfnd  9413  prcdnq  9800  dfrtrcl2  13783  relexpindlem  13784  bnj1379  30875  bnj1052  31017  bnj1118  31026  bnj1154  31041  bnj1280  31062  dftrcl3  37831  dfrtrcl3  37844  vk15.4j  38554  hbimpg  38590
  Copyright terms: Public domain W3C validator