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

Theorem nfan 1544
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 1543 1 𝑥(𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wa 103  wnf 1436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487
This theorem depends on definitions:  df-bi 116  df-nf 1437
This theorem is referenced by:  nf3an  1545  cbvex2  1894  nfsbxyt  1916  sbcomxyyz  1945  nfsb4t  1989  clelab  2265  nfel  2290  2ralbida  2456  r19.29an  2574  reean  2599  nfrabxy  2611  cbvrexf  2649  cbvreu  2652  cbvrab  2684  ceqsex2  2726  vtocl2gaf  2753  rspce  2784  eqvincf  2810  elrabf  2838  elrab3t  2839  rexab2  2850  morex  2868  reu2  2872  rmo3f  2881  sbc2iegf  2979  rmo2ilem  2998  rmo3  3000  csbiebt  3039  csbie2t  3048  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  nfopd  3722  eluniab  3748  dfnfc2  3754  nfdisjv  3918  disjiun  3924  nfopab  3996  cbvopab  3999  cbvopab1  4001  cbvopab2  4002  cbvopab1s  4003  mpteq12f  4008  nfmpt  4020  cbvmptf  4022  cbvmpt  4023  repizf2  4086  nfpo  4223  nfso  4224  nfwe  4277  onintonm  4433  peano2  4509  nfxp  4566  opeliunxp  4594  nfco  4704  elrnmpt1  4790  nfimad  4890  iota2  5114  dffun4f  5139  nffun  5146  imadif  5203  funimaexglem  5206  nffn  5219  nff  5269  nff1  5326  nffo  5344  nff1o  5365  fun11iun  5388  nffvd  5433  fv3  5444  fmptco  5586  nfiso  5707  cbvriota  5740  riota2df  5750  riota5f  5754  nfoprab  5823  mpoeq123  5830  nfmpo  5840  cbvoprab1  5843  cbvoprab2  5844  cbvoprab12  5845  cbvoprab3  5847  cbvmpox  5849  ovmpodxf  5896  opabex3d  6019  opabex3  6020  dfoprab4f  6091  fmpox  6098  spc2ed  6130  cnvoprab  6131  f1od2  6132  opeliunxp2f  6135  nfrecs  6204  tfri3  6264  nffrec  6293  erovlem  6521  nfixpxy  6611  nfixp1  6612  xpf1o  6738  nneneq  6751  ac6sfi  6792  nfsup  6879  exmidomni  7014  fodjuomnilemdc  7016  ismkvnex  7029  mkvprop  7032  exmidfodomrlemr  7063  exmidfodomrlemrALT  7064  cc3  7088  caucvgsrlemgt1  7615  suplocsrlem  7628  axpre-suploclemres  7721  supinfneg  9402  infsupneg  9403  fimaxre2  11010  nfsum1  11137  nfsum  11138  fsumsplitf  11189  fsum2dlemstep  11215  fsum00  11243  nfcprod1  11335  nfcprod  11336  prodeq2  11338  zsupcllemstep  11649  bezoutlemmain  11697  bezoutlemzz  11701  bezout  11710  exmidunben  11950  ctiunctlemfo  11963  ctiunct  11964  mulcncf  12774  ellimc3apf  12812  limccnp2cntop  12829  bdsepnft  13169  bdsepnfALT  13171  bj-findis  13261  strcollnft  13266  pw1nct  13282  isomninnlem  13311  trirec0  13323
  Copyright terms: Public domain W3C validator