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

Theorem 19.21bi 2047
 Description: Inference form of 19.21 2062 and also deduction form of sp 2041. (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 2041 . 2 (∀𝑥𝜓𝜓)
31, 2syl 17 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1473 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-ex 1696 This theorem is referenced by:  19.21bbi  2048  eqeq1dALT  2613  eleq2dALT  2675  ssel  3562  pocl  4966  funmo  5820  funun  5846  fununi  5878  findcard  8084  findcard2  8085  axpowndlem4  9301  axregndlem2  9304  axinfnd  9307  prcdnq  9694  dfrtrcl2  13650  relexpindlem  13651  bnj1379  30155  bnj1052  30297  bnj1118  30306  bnj1154  30321  bnj1280  30342  dftrcl3  37031  dfrtrcl3  37044  vk15.4j  37755  hbimpg  37791
 Copyright terms: Public domain W3C validator