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

Theorem nfim 1781
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 1773 . 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 1534
This theorem is referenced by:  nfor  1782  nfan  1783  nfbi  1784  nfia1  1790  19.38  1822  nfmo1  2167  mo  2178  moexex  2225  2mo  2234  2eu4  2239  2eu6  2241  cbvralf  2771  vtocl2gf  2858  vtocl3gf  2859  vtoclgaf  2861  vtocl2gaf  2863  vtocl3gaf  2865  rspct  2890  rspc  2891  ralab2  2943  mob  2960  csbhypf  3129  cbvralcsf  3156  dfss2f  3184  elintab  3889  axrep2  4149  axrep3  4150  nfpo  4335  nffr  4383  reusv2lem4  4554  reusv3  4558  tfis  4661  tfinds  4666  tfindes  4669  findes  4702  fv3  5557  tz6.12c  5563  fvmptss  5625  fvmptdf  5627  fvmptt  5631  fvmptf  5632  fmptco  5707  dff13f  5800  ovmpt2s  5987  ov2gf  5988  ovmpt2df  5995  ov3  6000  dfoprab4f  6194  tfr3  6431  dom2lem  6917  findcard2  7114  ac6sfi  7117  dfac8clem  7675  aceq1  7760  dfac5lem5  7770  zfcndrep  8252  zfcndinf  8256  pwfseqlem4a  8299  pwfseqlem4  8300  uzindOLD  10122  uzind4s  10294  rlim2  11986  ello1mpt  12011  o1compt  12077  summolem2a  12204  sumss  12213  o1fsum  12287  prmind2  12785  mreiincl  13514  gsumcom2  15242  ptcldmpt  17324  cnmptcom  17388  elmptrab  17538  isfildlem  17568  dvmptfsum  19338  dvfsumlem2  19390  dvfsumlem4  19392  dvfsumrlim  19394  dvfsum2  19397  coeeq2  19640  dgrle  19641  rlimcnp  20276  lgseisenlem2  20605  dchrisumlema  20653  dchrisumlem2  20655  dchrisumlem3  20656  isch3  21837  atom1d  22949  mo5f  23159  ssiun2sf  23173  fmptcof2  23244  measiun  23560  prodmolem2a  24157  setinds  24205  tfisg  24275  wfisg  24280  frinsg  24316  mptelee  24595  bwt2  25695  subtr  26327  subtr2  26328  fdc1  26559  fphpd  27002  monotuz  27129  monotoddzz  27131  oddcomabszz  27132  setindtrs  27221  aomclem6  27259  flcidc  27482  fmul01  27813  fmuldfeqlem1  27815  fmuldfeq  27816  fmul01lt1lem1  27817  fmul01lt1lem2  27818  climmulf  27833  climexp  27834  climsuse  27837  climrecf  27838  climinff  27840  stoweidlem3  27855  stoweidlem26  27878  stoweidlem31  27883  stoweidlem34  27886  stoweidlem42  27894  stoweidlem43  27895  stoweidlem48  27900  stoweidlem51  27903  stoweidlem59  27911  2reu4a  28070  eu2ndop1stv  28083  bnj1385  29181  bnj1468  29194  bnj110  29206  bnj849  29273  bnj900  29277  bnj981  29298  bnj1014  29308  bnj1123  29332  bnj1128  29336  bnj1384  29378  bnj1489  29402  bnj1497  29406  cdleme31sn1  31192  cdleme32fva  31248  cdlemk36  31724
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-tru 1310  df-nf 1535
  Copyright terms: Public domain W3C validator