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

Theorem nfim 1505
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 1504 1  |-  F/ x
( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1390
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 1377  ax-gen 1379  ax-4 1441  ax-ial 1468  ax-i5r 1469
This theorem depends on definitions:  df-bi 115  df-nf 1391
This theorem is referenced by:  nfnf  1510  nfia1  1513  sb4or  1756  cbval2  1839  nfmo1  1955  mo23  1984  euexex  2028  cbvralf  2576  vtocl2gf  2669  vtocl3gf  2670  vtoclgaf  2672  vtocl2gaf  2674  vtocl3gaf  2676  rspct  2703  rspc  2704  ralab2  2765  mob  2783  csbhypf  2950  cbvralcsf  2973  dfss2f  2999  elintab  3667  nfpo  4084  nfso  4085  nffrfor  4131  frind  4135  nfwe  4138  reusv3  4238  tfis  4352  findes  4372  dffun4f  4968  fv3  5249  tz6.12c  5255  fvmptss2  5299  fvmptssdm  5307  fvmptdf  5310  fvmptt  5314  fvmptf  5315  fmptco  5382  dff13f  5461  ovmpt2s  5675  ov2gf  5676  ovmpt2df  5683  ovi3  5688  dfoprab4f  5870  tfri3  6036  dom2lem  6340  findcard2  6445  findcard2s  6446  ac6sfi  6454  nfsup  6499  uzind4s  8811  indstr  8814  supinfneg  8816  infsupneg  8817  uzsinds  9570  fimaxre2  10310  divalglemeunn  10528  divalglemeuneg  10530  zsupcllemstep  10548  bezoutlemmain  10594  prmind2  10709  elabgft1  10848  elabgf2  10850  bj-rspgt  10856  bj-bdfindes  11011  setindis  11029  bdsetindis  11031  bj-findis  11041  bj-findes  11043
  Copyright terms: Public domain W3C validator