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 2189
Description: Inference form of 19.21 2207 and also deduction form of sp 2183. (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 2183 . 2 (∀𝑥𝜓𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  19.21bbi  2190  axc7e  2318  eleq2w2  2733  eqeq1dALT  2740  eleq2dALT  2828  nfeqd  2916  funmoOLD  6582  funun  6612  fununi  6641  findcard  9203  findcard2  9204  ssfi  9213  ttrclselem2  9766  axpowndlem4  10640  axregndlem2  10643  axinfnd  10646  prcdnq  11033  dfrtrcl2  15101  relexpindlem  15102  bnj1379  34844  bnj1052  34989  bnj1118  34998  bnj1154  35013  bnj1280  35034  gblacfnacd  35113  dftrcl3  43733  dfrtrcl3  43746  vk15.4j  44548  hbimpg  44574  pgindnf  49235
  Copyright terms: Public domain W3C validator