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

Theorem 19.21t 1814
 Description: Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
Assertion
Ref Expression
19.21t

Proof of Theorem 19.21t
StepHypRef Expression
1 nfr 1778 . . 3
2 ax-5 1567 . . 3
31, 2syl9 69 . 2
4 19.9t 1794 . . . 4
54imbi1d 310 . . 3
6 19.38 1813 . . 3
75, 6syl6bir 222 . 2
83, 7impbid 185 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178  wal 1550  wex 1551  wnf 1554 This theorem is referenced by:  19.21  1815  nfimd  1828  sbcom  2166  sbcomOLD  2167  sbal2  2213  ax11indalem  2276  ax11inda2ALT  2277  r19.21t  2793  ceqsalt  2980  sbciegft  3193  sbcomwAUX7  29662  sbcomOLD7  29829  sbal2OLD7  29842 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762 This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555
 Copyright terms: Public domain W3C validator