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

Theorem 19.21bi 1869
Description: Inference form of 19.21 1905 and also deduction form of sp 1859. (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 1859 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393
This theorem is referenced by:  19.21bbi  1870  equveliOLD  2089  2ax6e  2194  eqeq1dALT  2460  eqeq1OLD  2462  eleq2dALT  2528  eleq2OLD  2532  r19.21biOLD  2827  elrab3t  3256  ssel  3497  pocl  4812  funmo  5609  funun  5635  fununi  5659  findcard  7779  findcard2  7780  axpowndlem2OLD  8995  axpowndlem4  8998  axregndlem2  9001  axinfnd  9005  prcdnq  9392  relexpindlem  29062  dfrtrcl2  29071  vk15.4j  33298  hbimpg  33327  bnj1379  33889  bnj1052  34031  bnj1118  34040  bnj1154  34055  bnj1280  34076
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator