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 2046
Description: Inference form of 19.21 2061 and also deduction form of sp 2040. (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 2040 . 2 (∀𝑥𝜓𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  19.21bbi  2047  eqeq1dALT  2612  eleq2dALT  2674  ssel  3561  pocl  4956  funmo  5806  funun  5832  fununi  5864  findcard  8061  findcard2  8062  axpowndlem4  9278  axregndlem2  9281  axinfnd  9284  prcdnq  9671  dfrtrcl2  13596  relexpindlem  13597  bnj1379  29961  bnj1052  30103  bnj1118  30112  bnj1154  30127  bnj1280  30148  dftrcl3  36827  dfrtrcl3  36840  vk15.4j  37551  hbimpg  37587
  Copyright terms: Public domain W3C validator