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

Theorem nfimd 1925
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 1907 . . . 4  |-  F/ x F/ x ps
4 nfnf1 1907 . . . 4  |-  F/ x F/ x ch
5 nfr 1881 . . . . . 6  |-  ( F/ x ch  ->  ( ch  ->  A. x ch )
)
65imim2d 52 . . . . 5  |-  ( F/ x ch  ->  (
( ps  ->  ch )  ->  ( ps  ->  A. x ch ) ) )
7 19.21t 1912 . . . . . 6  |-  ( F/ x ps  ->  ( A. x ( ps  ->  ch )  <->  ( ps  ->  A. x ch ) ) )
87biimprd 223 . . . . 5  |-  ( F/ x ps  ->  (
( ps  ->  A. x ch )  ->  A. x
( ps  ->  ch ) ) )
96, 8syl9r 72 . . . 4  |-  ( F/ x ps  ->  ( F/ x ch  ->  (
( ps  ->  ch )  ->  A. x ( ps 
->  ch ) ) ) )
103, 4, 9alrimd 1889 . . 3  |-  ( F/ x ps  ->  ( F/ x ch  ->  A. x
( ( ps  ->  ch )  ->  A. x
( ps  ->  ch ) ) ) )
11 df-nf 1625 . . 3  |-  ( F/ x ( ps  ->  ch )  <->  A. x ( ( ps  ->  ch )  ->  A. x ( ps 
->  ch ) ) )
1210, 11syl6ibr 227 . 2  |-  ( F/ x ps  ->  ( F/ x ch  ->  F/ x ( ps  ->  ch ) ) )
131, 2, 12sylc 60 1  |-  ( ph  ->  F/ x ( ps 
->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1397   F/wnf 1624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-12 1862
This theorem depends on definitions:  df-bi 185  df-ex 1621  df-nf 1625
This theorem is referenced by:  hbimd  1929  nfand  1933  nfbid  1941  dvelimhw  1963  dvelimf  2082  nfmod2  2233  nfrald  2767  nfifd  3885  nfixp  7407  axrepndlem1  8880  axrepndlem2  8881  axunndlem1  8883  axunnd  8884  axpowndlem2  8886  axpowndlem3  8887  axpowndlem4  8888  axregndlem2  8891  axregnd  8892  axregndOLD  8893  axinfndlem1  8894  axinfnd  8895  axacndlem4  8899  axacndlem5  8900  axacnd  8901  wl-mo2dnae  30184  wl-mo2t  30185  riotasv2d  35101
  Copyright terms: Public domain W3C validator