NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfan GIF version

Theorem nfan 1824
Description: If x is not free in φ and ψ, it is not free in (φ ψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortned by Wolf Lammen, 2-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 . . . 4 xφ
21a1i 10 . . 3 ( ⊤ → Ⅎxφ)
3 nfan.2 . . . 4 xψ
43a1i 10 . . 3 ( ⊤ → Ⅎxψ)
52, 4nfand 1822 . 2 ( ⊤ → Ⅎx(φ ψ))
65trud 1323 1 x(φ ψ)
Colors of variables: wff setvar class
Syntax hints:   wa 358  wtru 1316  wnf 1544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545
This theorem is referenced by:  nfnan  1825  nf3an  1827  hban  1828  nfbiOLD  1835  nfeqf  1958  nfald2  1972  spimt  1974  dvelimf  1997  cbval2  2004  cbvex2  2005  nfsb4t  2080  dvelimdf  2082  sbcom  2089  nfeud2  2216  mopick  2266  eupicka  2268  mopick2  2271  2eu6  2289  clelab  2473  nfel  2497  nfabd2  2507  2ralbida  2653  ralcom2  2775  reean  2777  cbvreu  2833  cbvrab  2857  ceqsex2  2895  vtocl2gaf  2921  rspce  2950  eqvincf  2967  elrabf  2993  rexab2  3003  morex  3020  reu2  3024  sbc2iegf  3112  rmo2  3131  rmo3  3133  csbiebt  3172  csbie2t  3180  cbvreucsf  3200  cbvrabcsf  3201  eluniab  3903  dfnfc2  3909  iota2  4367  ncfinraise  4481  ncfinlower  4483  nfopd  4605  nfopab  4627  cbvopab  4630  cbvopab1  4632  cbvopab2  4633  cbvopab1s  4634  nfxp  4810  opeliunxp  4820  nfco  4882  nfimad  4954  imadif  5171  nffn  5180  nff  5221  nff1  5256  nffo  5268  nff1o  5285  fun11iun  5305  nffvd  5335  fv3  5341  nfiso  5487  nfoprab  5549  cbvoprab1  5567  cbvoprab2  5568  cbvoprab12  5569  cbvoprab3  5571  mpteq12f  5655  mpt2eq123  5661  nfmpt  5671  nfmpt2  5675  cbvmpt  5676  cbvmpt2x  5678  fmpt2x  5730
  Copyright terms: Public domain W3C validator