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

Theorem 19.23t 1776
 Description: Closed form of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 7-Nov-2005.)
Assertion
Ref Expression
19.23t

Proof of Theorem 19.23t
StepHypRef Expression
1 exim 1573 . . 3
2 19.9t 1761 . . . 4
32imbi2d 309 . . 3
41, 3syl5ib 212 . 2
5 nfnf1 1720 . . 3
6 nfe1 1566 . . . . 5
76a1i 12 . . . 4
8 id 21 . . . 4
97, 8nfimd 1727 . . 3
10 19.8a 1758 . . . . 5
1110a1i 12 . . . 4
1211imim1d 71 . . 3
135, 9, 12alrimdd 1709 . 2
144, 13impbid 185 1
 Colors of variables: wff set class Syntax hints:   wi 6   wb 178  wal 1532  wex 1537  wnf 1539 This theorem is referenced by:  19.23  1777  sbft  1897  r19.23t  2619  ceqsalt  2748  vtoclgft  2772  sbciegft  2951 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-4 1692 This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
 Copyright terms: Public domain W3C validator