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

Theorem nfan 1473
Description: If 𝑥 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 𝑥𝜑
nfan.2 𝑥𝜓
Assertion
Ref Expression
nfan 𝑥(𝜑𝜓)

Proof of Theorem nfan
StepHypRef Expression
1 nfan.1 . 2 𝑥𝜑
2 nfan.2 . . 3 𝑥𝜓
32a1i 9 . 2 (𝜑 → Ⅎ𝑥𝜓)
41, 3nfan1 1472 1 𝑥(𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wa 101  wnf 1365
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416
This theorem depends on definitions:  df-bi 114  df-nf 1366
This theorem is referenced by:  nf3an  1474  cbvex2  1813  nfsbxyt  1835  sbcomxyyz  1862  nfsb4t  1906  clelab  2178  nfel  2202  2ralbida  2362  reean  2495  nfrabxy  2507  cbvrexf  2545  cbvreu  2548  cbvrab  2572  ceqsex2  2611  vtocl2gaf  2637  rspce  2668  eqvincf  2691  elrabf  2718  elrab3t  2719  rexab2  2729  morex  2747  reu2  2751  sbc2iegf  2855  rmo2ilem  2874  rmo3  2876  csbiebt  2913  csbie2t  2921  cbvrexcsf  2936  cbvreucsf  2937  cbvrabcsf  2938  nfopd  3593  eluniab  3619  dfnfc2  3625  nfdisjv  3784  nfopab  3852  cbvopab  3855  cbvopab1  3857  cbvopab2  3858  cbvopab1s  3859  mpteq12f  3864  nfmpt  3876  cbvmpt  3878  repizf2  3942  nfpo  4065  nfso  4066  nfwe  4119  onintonm  4270  peano2  4345  nfxp  4398  opeliunxp  4422  nfco  4528  elrnmpt1  4612  nfimad  4704  iota2  4920  dffun4f  4945  nffun  4951  imadif  5006  funimaexglem  5009  nffn  5022  nff  5070  nff1  5117  nffo  5132  nff1o  5151  fun11iun  5174  nffvd  5214  fv3  5224  fmptco  5357  nfiso  5473  cbvriota  5505  riota2df  5515  riota5f  5519  nfoprab  5584  mpt2eq123  5591  nfmpt2  5600  cbvoprab1  5603  cbvoprab2  5604  cbvoprab12  5605  cbvoprab3  5607  cbvmpt2x  5609  ovmpt2dxf  5653  opabex3d  5775  opabex3  5776  dfoprab4f  5846  fmpt2x  5853  spc2ed  5881  cnvoprab  5882  f1od2  5883  nfrecs  5952  tfri3  5983  nffrec  6012  erovlem  6228  nneneq  6350  ac6sfi  6382  nfsup  6397  caucvgsrlemgt1  6936  nfsum1  10098  nfsum  10099  bdsepnft  10366  bdsepnfALT  10368  bj-findis  10463  strcollnft  10468
  Copyright terms: Public domain W3C validator