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

Theorem nfimd 1761
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 1756 . . . . 5  |-  F/ x A. x ( ps  ->  A. x ps )
4 hbnt 1724 . . . . . 6  |-  ( A. x ( ps  ->  A. x ps )  -> 
( -.  ps  ->  A. x  -.  ps )
)
5 pm2.21 100 . . . . . . . . . . 11  |-  ( -. 
ps  ->  ( ps  ->  ch ) )
65alimi 1546 . . . . . . . . . 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 1546 . . . . . . . . . 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 1744 . . . 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 1532 . . . 4  |-  ( F/ x ps  <->  A. x
( ps  ->  A. x ps ) )
19 df-nf 1532 . . . 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 1532 . . 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 1527   F/wnf 1531
This theorem is referenced by:  nfbid  1762  nfand  1763  nfnf  1768  nfim  1769  19.21t  1790  19.23t  1796  dvelimf  1937  nfsb4t  2020  nfmod2  2156  nfrald  2594  nfifd  3588  riotasvdOLD  6348  riotasv2d  6349  riotasv2dOLD  6350  nfixp  6835  axrepndlem1  8214  axrepndlem2  8215  axunndlem1  8217  axunnd  8218  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axregndlem2  8225  axregnd  8226  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234  a12lem1  28503
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532
  Copyright terms: Public domain W3C validator