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

Theorem nfim 1769
Description: If  x is not free in  ph and  ps, it is not free in  ( ph  ->  ps ). (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nf.1  |-  F/ x ph
nf.2  |-  F/ x ps
Assertion
Ref Expression
nfim  |-  F/ x
( ph  ->  ps )

Proof of Theorem nfim
StepHypRef Expression
1 nf.1 . . . 4  |-  F/ x ph
21a1i 10 . . 3  |-  (  T. 
->  F/ x ph )
3 nf.2 . . . 4  |-  F/ x ps
43a1i 10 . . 3  |-  (  T. 
->  F/ x ps )
52, 4nfimd 1761 . 2  |-  (  T. 
->  F/ x ( ph  ->  ps ) )
65trud 1314 1  |-  F/ x
( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    T. wtru 1307   F/wnf 1531
This theorem is referenced by:  nfor  1770  nfan  1771  nfbi  1772  nfia1  1778  19.38  1810  nfmo1  2154  mo  2165  moexex  2212  2mo  2221  2eu4  2226  2eu6  2228  cbvralf  2758  vtocl2gf  2845  vtocl3gf  2846  vtoclgaf  2848  vtocl2gaf  2850  vtocl3gaf  2852  rspct  2877  rspc  2878  ralab2  2930  mob  2947  csbhypf  3116  cbvralcsf  3143  dfss2f  3171  elintab  3873  axrep2  4133  axrep3  4134  nfpo  4319  nffr  4367  reusv2lem4  4538  reusv3  4542  tfis  4645  tfinds  4650  tfindes  4653  findes  4686  fv3  5541  tz6.12c  5547  fvmptss  5609  fvmptdf  5611  fvmptt  5615  fvmptf  5616  fmptco  5691  dff13f  5784  ovmpt2s  5971  ov2gf  5972  ovmpt2df  5979  ov3  5984  dfoprab4f  6178  tfr3  6415  dom2lem  6901  findcard2  7098  ac6sfi  7101  dfac8clem  7659  aceq1  7744  dfac5lem5  7754  zfcndrep  8236  zfcndinf  8240  pwfseqlem4a  8283  pwfseqlem4  8284  uzindOLD  10106  uzind4s  10278  rlim2  11970  ello1mpt  11995  o1compt  12061  summolem2a  12188  sumss  12197  o1fsum  12271  prmind2  12769  mreiincl  13498  gsumcom2  15226  ptcldmpt  17308  cnmptcom  17372  elmptrab  17522  isfildlem  17552  dvmptfsum  19322  dvfsumlem2  19374  dvfsumlem4  19376  dvfsumrlim  19378  dvfsum2  19381  coeeq2  19624  dgrle  19625  rlimcnp  20260  lgseisenlem2  20589  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  isch3  21821  atom1d  22933  mo5f  23143  ssiun2sf  23157  fmptcof2  23229  measiun  23545  setinds  24134  tfisg  24204  wfisg  24209  frinsg  24245  mptelee  24523  bwt2  25592  subtr  26224  subtr2  26225  fdc1  26456  fphpd  26899  monotuz  27026  monotoddzz  27028  oddcomabszz  27029  setindtrs  27118  aomclem6  27156  flcidc  27379  fmul01  27710  fmuldfeqlem1  27712  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  climmulf  27730  climexp  27731  climsuse  27734  climrecf  27735  climinff  27737  stoweidlem3  27752  stoweidlem26  27775  stoweidlem31  27780  stoweidlem34  27783  stoweidlem42  27791  stoweidlem43  27792  stoweidlem48  27797  stoweidlem51  27800  stoweidlem59  27808  2reu4a  27967  bnj1385  28865  bnj1468  28878  bnj110  28890  bnj849  28957  bnj900  28961  bnj981  28982  bnj1014  28992  bnj1123  29016  bnj1128  29020  bnj1384  29062  bnj1489  29086  bnj1497  29090  cdleme31sn1  30570  cdleme32fva  30626  cdlemk36  31102
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-tru 1310  df-nf 1532
  Copyright terms: Public domain W3C validator