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

Theorem nfimd 2010
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 1991 . . . 4  |-  F/ x F/ x ps
4 nfnf1 1991 . . . 4  |-  F/ x F/ x ch
5 nfr 1961 . . . . . 6  |-  ( F/ x ch  ->  ( ch  ->  A. x ch )
)
65imim2d 54 . . . . 5  |-  ( F/ x ch  ->  (
( ps  ->  ch )  ->  ( ps  ->  A. x ch ) ) )
7 19.21t 1996 . . . . . 6  |-  ( F/ x ps  ->  ( A. x ( ps  ->  ch )  <->  ( ps  ->  A. x ch ) ) )
87biimprd 231 . . . . 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 1969 . . 3  |-  ( F/ x ps  ->  ( F/ x ch  ->  A. x
( ( ps  ->  ch )  ->  A. x
( ps  ->  ch ) ) ) )
11 df-nf 1678 . . 3  |-  ( F/ x ( ps  ->  ch )  <->  A. x ( ( ps  ->  ch )  ->  A. x ( ps 
->  ch ) ) )
1210, 11syl6ibr 235 . 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 1452   F/wnf 1677
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-12 1943
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-nf 1678
This theorem is referenced by:  hbimd  2014  nfand  2018  nfbid  2026  dvelimhw  2070  dvelimf  2178  nfmod2  2322  nfrald  2784  nfifd  3920  nfixp  7566  axrepndlem1  9042  axrepndlem2  9043  axunndlem1  9045  axunnd  9046  axpowndlem2  9048  axpowndlem3  9049  axpowndlem4  9050  axregndlem2  9053  axregnd  9054  axinfndlem1  9055  axinfnd  9056  axacndlem4  9060  axacndlem5  9061  axacnd  9062  wl-mo2df  31943  wl-mo2t  31948  riotasv2d  32573
  Copyright terms: Public domain W3C validator