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

Theorem nfimd 1859
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 1842 . . . 4  |-  F/ x F/ x ps
4 nfnf1 1842 . . . 4  |-  F/ x F/ x ch
5 nfr 1816 . . . . . 6  |-  ( F/ x ch  ->  ( ch  ->  A. x ch )
)
65imim2d 52 . . . . 5  |-  ( F/ x ch  ->  (
( ps  ->  ch )  ->  ( ps  ->  A. x ch ) ) )
7 19.21t 1847 . . . . . 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 1824 . . 3  |-  ( F/ x ps  ->  ( F/ x ch  ->  A. x
( ( ps  ->  ch )  ->  A. x
( ps  ->  ch ) ) ) )
11 df-nf 1595 . . 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 1372   F/wnf 1594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-12 1798
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-nf 1595
This theorem is referenced by:  hbimd  1863  nfand  1867  nfbid  1875  dvelimhw  1897  dvelimf  2044  nfmod2  2286  nfrald  2844  nfifd  3962  nfixp  7480  axrepndlem1  8958  axrepndlem2  8959  axunndlem1  8961  axunnd  8962  axpowndlem2  8964  axpowndlem2OLD  8965  axpowndlem3  8966  axpowndlem3OLD  8967  axpowndlem4  8968  axregndlem2  8971  axregnd  8972  axregndOLD  8973  axinfndlem1  8974  axinfnd  8975  axacndlem4  8979  axacndlem5  8980  axacnd  8981  wl-mo2dnae  29584  wl-mo2t  29585  riotasv2d  33637
  Copyright terms: Public domain W3C validator