ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfim Unicode version

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

Proof of Theorem nfim
StepHypRef Expression
1 nfim.1 . 2  |-  F/ x ph
2 nfim.2 . . 3  |-  F/ x ps
32a1i 9 . 2  |-  ( ph  ->  F/ x ps )
41, 3nfim1 1508 1  |-  F/ x
( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1394
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-ial 1472  ax-i5r 1473
This theorem depends on definitions:  df-bi 115  df-nf 1395
This theorem is referenced by:  nfnf  1514  nfia1  1517  sb4or  1761  cbval2  1844  nfmo1  1960  mo23  1989  euexex  2033  cbvralf  2584  vtocl2gf  2681  vtocl3gf  2682  vtoclgaf  2684  vtocl2gaf  2686  vtocl3gaf  2688  rspct  2715  rspc  2716  ralab2  2777  mob  2795  csbhypf  2964  cbvralcsf  2988  dfss2f  3014  elintab  3694  disjiun  3832  nfpo  4119  nfso  4120  nffrfor  4166  frind  4170  nfwe  4173  reusv3  4273  tfis  4388  findes  4408  omsinds  4425  dffun4f  5018  fv3  5312  tz6.12c  5318  fvmptss2  5363  fvmptssdm  5371  fvmptdf  5374  fvmptt  5378  fvmptf  5379  fmptco  5448  dff13f  5531  ovmpt2s  5750  ov2gf  5751  ovmpt2df  5758  ovi3  5763  dfoprab4f  5945  tfri3  6114  dom2lem  6469  findcard2  6585  findcard2s  6586  ac6sfi  6594  nfsup  6666  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  uzind4s  9047  indstr  9050  supinfneg  9052  infsupneg  9053  uzsinds  9813  fimaxre2  10622  isummolem2a  10735  fsumsplitf  10765  divalglemeunn  11014  divalglemeuneg  11016  zsupcllemstep  11034  bezoutlemmain  11080  prmind2  11195  elabgft1  11335  elabgf2  11337  bj-rspgt  11343  bj-bdfindes  11501  setindis  11519  bdsetindis  11521  bj-findis  11531  bj-findes  11533
  Copyright terms: Public domain W3C validator