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

Theorem nfimd 1773
Description: If  x is not free in  ph and  ps, it is not free in  ( ph  ->  ps ). (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
nfnd.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 nfnd.1 . 2  |-  ( ph  ->  F/ x ps )
2 nfimd.2 . 2  |-  ( ph  ->  F/ x ch )
3 nfa1 1768 . . . . 5  |-  F/ x A. x ( ps  ->  A. x ps )
4 hbnt 1736 . . . . . 6  |-  ( A. x ( ps  ->  A. x ps )  -> 
( -.  ps  ->  A. x  -.  ps )
)
5 pm2.21 100 . . . . . . . . . . 11  |-  ( -. 
ps  ->  ( ps  ->  ch ) )
65alimi 1549 . . . . . . . . . 10  |-  ( A. x  -.  ps  ->  A. x
( ps  ->  ch ) )
76imim2i 13 . . . . . . . . 9  |-  ( ( -.  ps  ->  A. x  -.  ps )  ->  ( -.  ps  ->  A. x
( ps  ->  ch ) ) )
87adantr 451 . . . . . . . 8  |-  ( ( ( -.  ps  ->  A. x  -.  ps )  /\  ( ch  ->  A. x ch ) )  ->  ( -.  ps  ->  A. x
( ps  ->  ch ) ) )
9 ax-1 5 . . . . . . . . . . 11  |-  ( ch 
->  ( ps  ->  ch ) )
109alimi 1549 . . . . . . . . . 10  |-  ( A. x ch  ->  A. x
( ps  ->  ch ) )
1110imim2i 13 . . . . . . . . 9  |-  ( ( ch  ->  A. x ch )  ->  ( ch 
->  A. x ( ps 
->  ch ) ) )
1211adantl 452 . . . . . . . 8  |-  ( ( ( -.  ps  ->  A. x  -.  ps )  /\  ( ch  ->  A. x ch ) )  ->  ( ch  ->  A. x ( ps 
->  ch ) ) )
138, 12jad 154 . . . . . . 7  |-  ( ( ( -.  ps  ->  A. x  -.  ps )  /\  ( ch  ->  A. x ch ) )  ->  (
( ps  ->  ch )  ->  A. x ( ps 
->  ch ) ) )
1413ex 423 . . . . . 6  |-  ( ( -.  ps  ->  A. x  -.  ps )  ->  (
( ch  ->  A. x ch )  ->  ( ( ps  ->  ch )  ->  A. x ( ps 
->  ch ) ) ) )
154, 14syl 15 . . . . 5  |-  ( A. x ( ps  ->  A. x ps )  -> 
( ( ch  ->  A. x ch )  -> 
( ( ps  ->  ch )  ->  A. x
( ps  ->  ch ) ) ) )
163, 15alimd 1756 . . . 4  |-  ( A. x ( ps  ->  A. x ps )  -> 
( A. x ( ch  ->  A. x ch )  ->  A. x
( ( ps  ->  ch )  ->  A. x
( ps  ->  ch ) ) ) )
1716imp 418 . . 3  |-  ( ( A. x ( ps 
->  A. x ps )  /\  A. x ( ch 
->  A. x ch )
)  ->  A. x
( ( ps  ->  ch )  ->  A. x
( ps  ->  ch ) ) )
18 df-nf 1535 . . . 4  |-  ( F/ x ps  <->  A. x
( ps  ->  A. x ps ) )
19 df-nf 1535 . . . 4  |-  ( F/ x ch  <->  A. x
( ch  ->  A. x ch ) )
2018, 19anbi12i 678 . . 3  |-  ( ( F/ x ps  /\  F/ x ch )  <->  ( A. x ( ps  ->  A. x ps )  /\  A. x ( ch  ->  A. x ch ) ) )
21 df-nf 1535 . . 3  |-  ( F/ x ( ps  ->  ch )  <->  A. x ( ( ps  ->  ch )  ->  A. x ( ps 
->  ch ) ) )
2217, 20, 213imtr4i 257 . 2  |-  ( ( F/ x ps  /\  F/ x ch )  ->  F/ x ( ps  ->  ch ) )
231, 2, 22syl2anc 642 1  |-  ( ph  ->  F/ x ( ps 
->  ch ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358   A.wal 1530   F/wnf 1534
This theorem is referenced by:  nfbid  1774  nfand  1775  nfnf  1780  nfim  1781  19.21t  1802  19.23t  1808  dvelimf  1950  nfsb4t  2033  nfmod2  2169  nfrald  2607  nfifd  3601  riotasvdOLD  6364  riotasv2d  6365  riotasv2dOLD  6366  nfixp  6851  axrepndlem1  8230  axrepndlem2  8231  axunndlem1  8233  axunnd  8234  axpowndlem2  8236  axpowndlem3  8237  axpowndlem4  8238  axregndlem2  8241  axregnd  8242  axinfndlem1  8243  axinfnd  8244  axacndlem4  8248  axacndlem5  8249  axacnd  8250  nfsb4twAUX7  29551  nfnfOLD7  29643  dvelimfOLD7  29681  nfsb4tOLD7  29699  nfsb4tw2AUXOLD7  29700  a12lem1  29752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1535
  Copyright terms: Public domain W3C validator