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

Theorem 19.21vOLDOLD 1789
 Description: Obsolete proof of 19.21v 1788 as of 12-Jul-2020. (Contributed by NM, 21-Jun-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
19.21vOLDOLD
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem 19.21vOLDOLD
StepHypRef Expression
1 ax-5 1760 . . 3
2 alim 1685 . . 3
31, 2syl5 33 . 2
4 ax5e 1762 . . . 4
54imim1i 60 . . 3
6 19.38 1714 . . 3
75, 6syl 17 . 2
83, 7impbii 191 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188  wal 1444  wex 1665 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760 This theorem depends on definitions:  df-bi 189  df-ex 1666 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator