ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfan Structured version   GIF version

Theorem nfan 1433
Description: If x is not free in φ and ψ, it is not free in (φ ψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.)
Hypotheses
Ref Expression
nfan.1 xφ
nfan.2 xψ
Assertion
Ref Expression
nfan x(φ ψ)

Proof of Theorem nfan
StepHypRef Expression
1 nfan.1 . 2 xφ
2 nfan.2 . . 3 xψ
32a1i 9 . 2 (φ → Ⅎxψ)
41, 3nfan1 1432 1 x(φ ψ)
Colors of variables: wff set class
Syntax hints:   wa 97  wnf 1325
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-gen 1314  ax-4 1376
This theorem depends on definitions:  df-bi 110  df-nf 1326
This theorem is referenced by:  nf3an  1434  cbvex2  1773  nfsbxyt  1795  sbcomxyyz  1822  nfsb4t  1866  clelab  2138  nfel  2162  2ralbida  2317  reean  2450  nfrabxy  2462  cbvrexf  2500  cbvreu  2503  cbvrab  2527  ceqsex2  2565  vtocl2gaf  2591  rspce  2622  eqvincf  2640  elrabf  2667  elrab3t  2668  rexab2  2678  morex  2696  reu2  2700  sbc2iegf  2799  rmo2ilem  2818  rmo3  2820  csbiebt  2857  csbie2t  2865  cbvrexcsf  2880  cbvreucsf  2881  cbvrabcsf  2882  nfopd  3532  eluniab  3558  dfnfc2  3564  nfdisjv  3723  nfopab  3791  cbvopab  3794  cbvopab1  3796  cbvopab2  3797  cbvopab1s  3798  mpteq12f  3803  nfmpt  3815  cbvmpt  3817  repizf2  3881  nfpo  4004  nfso  4005  peano2  4236  nfxp  4289  opeliunxp  4313  nfco  4419  elrnmpt1  4503  nfimad  4595  iota2  4811  dffun4f  4835  nffun  4841  imadif  4896  funimaexglem  4899  nffn  4912  nff  4960  nff1  5006  nffo  5021  nff1o  5040  fun11iun  5063  nffvd  5103  fv3  5113  fmptco  5246  nfiso  5362  cbvriota  5393  riota2df  5403  riota5f  5407  nfoprab  5471  mpt2eq123  5478  nfmpt2  5487  cbvoprab1  5490  cbvoprab2  5491  cbvoprab12  5492  cbvoprab3  5494  cbvmpt2x  5496  ovmpt2dxf  5540  opabex3d  5662  opabex3  5663  dfoprab4f  5733  fmpt2x  5740  nfrecs  5835  tfri3  5866  erovlem  6100  bdsepnft  8527  bdsepnfALT  8529  bj-findis  8615  strcollnft  8620
  Copyright terms: Public domain W3C validator