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

Theorem nfimd 1828
Description: If in a context  x is not free in  ps and  ch, it is not free in  ( ps  ->  ch ). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
Hypotheses
Ref Expression
nfimd.1  |-  ( ph  ->  F/ x ps )
nfimd.2  |-  ( ph  ->  F/ x ch )
Assertion
Ref Expression
nfimd  |-  ( ph  ->  F/ x ( ps 
->  ch ) )

Proof of Theorem nfimd
StepHypRef Expression
1 nfimd.1 . 2  |-  ( ph  ->  F/ x ps )
2 nfimd.2 . 2  |-  ( ph  ->  F/ x ch )
3 nfnf1 1809 . . . 4  |-  F/ x F/ x ps
4 nfnf1 1809 . . . 4  |-  F/ x F/ x ch
5 nfr 1778 . . . . . 6  |-  ( F/ x ch  ->  ( ch  ->  A. x ch )
)
65imim2d 51 . . . . 5  |-  ( F/ x ch  ->  (
( ps  ->  ch )  ->  ( ps  ->  A. x ch ) ) )
7 19.21t 1814 . . . . . 6  |-  ( F/ x ps  ->  ( A. x ( ps  ->  ch )  <->  ( ps  ->  A. x ch ) ) )
87biimprd 216 . . . . 5  |-  ( F/ x ps  ->  (
( ps  ->  A. x ch )  ->  A. x
( ps  ->  ch ) ) )
96, 8syl9r 70 . . . 4  |-  ( F/ x ps  ->  ( F/ x ch  ->  (
( ps  ->  ch )  ->  A. x ( ps 
->  ch ) ) ) )
103, 4, 9alrimd 1786 . . 3  |-  ( F/ x ps  ->  ( F/ x ch  ->  A. x
( ( ps  ->  ch )  ->  A. x
( ps  ->  ch ) ) ) )
11 df-nf 1555 . . 3  |-  ( F/ x ( ps  ->  ch )  <->  A. x ( ( ps  ->  ch )  ->  A. x ( ps 
->  ch ) ) )
1210, 11syl6ibr 220 . 2  |-  ( F/ x ps  ->  ( F/ x ch  ->  F/ x ( ps  ->  ch ) ) )
131, 2, 12sylc 59 1  |-  ( ph  ->  F/ x ( ps 
->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550   F/wnf 1554
This theorem is referenced by:  nfimOLD  1834  hbimd  1835  19.23tOLD  1839  nfand  1844  nfbid  1855  nfbidOLD  1856  nfnfOLD  1869  dvelimhw  1877  19.21tOLD  1887  ax12olem4  2009  dvelimf  2069  dvelimfOLD  2070  sbequi  2112  nfsb4tOLD  2130  nfmod2  2296  nfrald  2759  nfifd  3764  riotasvdOLD  6595  riotasv2d  6596  riotasv2dOLD  6597  nfixp  7083  axrepndlem1  8469  axrepndlem2  8470  axunndlem1  8472  axunnd  8473  axpowndlem2  8475  axpowndlem3  8476  axpowndlem4  8477  axregndlem2  8480  axregnd  8481  axinfndlem1  8482  axinfnd  8483  axacndlem4  8487  axacndlem5  8488  axacnd  8489  nfsb4twAUX7  29638  nfnfOLD7  29751  dvelimfOLD7  29789  nfsb4tOLD7  29807  nfsb4tw2AUXOLD7  29808
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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