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

Theorem nfimd 1977
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 1958 . . . 4  |-  F/ x F/ x ps
4 nfnf1 1958 . . . 4  |-  F/ x F/ x ch
5 nfr 1928 . . . . . 6  |-  ( F/ x ch  ->  ( ch  ->  A. x ch )
)
65imim2d 54 . . . . 5  |-  ( F/ x ch  ->  (
( ps  ->  ch )  ->  ( ps  ->  A. x ch ) ) )
7 19.21t 1963 . . . . . 6  |-  ( F/ x ps  ->  ( A. x ( ps  ->  ch )  <->  ( ps  ->  A. x ch ) ) )
87biimprd 226 . . . . 5  |-  ( F/ x ps  ->  (
( ps  ->  A. x ch )  ->  A. x
( ps  ->  ch ) ) )
96, 8syl9r 74 . . . 4  |-  ( F/ x ps  ->  ( F/ x ch  ->  (
( ps  ->  ch )  ->  A. x ( ps 
->  ch ) ) ) )
103, 4, 9alrimd 1936 . . 3  |-  ( F/ x ps  ->  ( F/ x ch  ->  A. x
( ( ps  ->  ch )  ->  A. x
( ps  ->  ch ) ) ) )
11 df-nf 1662 . . 3  |-  ( F/ x ( ps  ->  ch )  <->  A. x ( ( ps  ->  ch )  ->  A. x ( ps 
->  ch ) ) )
1210, 11syl6ibr 230 . 2  |-  ( F/ x ps  ->  ( F/ x ch  ->  F/ x ( ps  ->  ch ) ) )
131, 2, 12sylc 62 1  |-  ( ph  ->  F/ x ( ps 
->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1435   F/wnf 1661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-12 1909
This theorem depends on definitions:  df-bi 188  df-ex 1658  df-nf 1662
This theorem is referenced by:  hbimd  1981  nfand  1985  nfbid  1993  dvelimhw  2037  dvelimf  2142  nfmod2  2289  nfrald  2750  nfifd  3882  nfixp  7496  axrepndlem1  8968  axrepndlem2  8969  axunndlem1  8971  axunnd  8972  axpowndlem2  8974  axpowndlem3  8975  axpowndlem4  8976  axregndlem2  8979  axregnd  8980  axinfndlem1  8981  axinfnd  8982  axacndlem4  8986  axacndlem5  8987  axacnd  8988  wl-mo2df  31806  wl-mo2t  31811  riotasv2d  32441
  Copyright terms: Public domain W3C validator