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

Theorem nfimd 1852
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 1835 . . . 4  |-  F/ x F/ x ps
4 nfnf1 1835 . . . 4  |-  F/ x F/ x ch
5 nfr 1809 . . . . . 6  |-  ( F/ x ch  ->  ( ch  ->  A. x ch )
)
65imim2d 52 . . . . 5  |-  ( F/ x ch  ->  (
( ps  ->  ch )  ->  ( ps  ->  A. x ch ) ) )
7 19.21t 1840 . . . . . 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 1817 . . 3  |-  ( F/ x ps  ->  ( F/ x ch  ->  A. x
( ( ps  ->  ch )  ->  A. x
( ps  ->  ch ) ) ) )
11 df-nf 1591 . . 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 1368   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  hbimd  1856  nfand  1860  nfbid  1868  dvelimhw  1890  dvelimf  2033  nfmod2  2276  nfrald  2878  nfifd  3917  nfixp  7384  axrepndlem1  8859  axrepndlem2  8860  axunndlem1  8862  axunnd  8863  axpowndlem2  8865  axpowndlem2OLD  8866  axpowndlem3  8867  axpowndlem3OLD  8868  axpowndlem4  8869  axregndlem2  8872  axregnd  8873  axregndOLD  8874  axinfndlem1  8875  axinfnd  8876  axacndlem4  8880  axacndlem5  8881  axacnd  8882  wl-mo2dnae  28535  wl-mo2t  28536  riotasv2d  32916
  Copyright terms: Public domain W3C validator