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

Theorem nfal 1553
 Description: If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1487. (Revised by Gino Giotto, 25-Aug-2024.)
Hypothesis
Ref Expression
nfal.1
Assertion
Ref Expression
nfal

Proof of Theorem nfal
StepHypRef Expression
1 df-nf 1438 . . . . . 6
21biimpi 119 . . . . 5
32alimi 1432 . . . 4
4 ax-7 1425 . . . 4
5 ax-5 1424 . . . . . 6
6 ax-7 1425 . . . . . 6
75, 6syl6 33 . . . . 5
87alimi 1432 . . . 4
93, 4, 83syl 17 . . 3
10 df-nf 1438 . . 3
119, 10sylibr 133 . 2
12 nfal.1 . 2
1311, 12mpg 1428 1
 Colors of variables: wff set class Syntax hints:   wi 4  wal 1330  wnf 1437 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 1424  ax-7 1425  ax-gen 1426 This theorem depends on definitions:  df-bi 116  df-nf 1438 This theorem is referenced by:  nfnf  1554  nfa2  1556  aaan  1564  cbv3  1719  cbv2  1726  nfald  1737  cbval2  1898  nfsb4t  1991  nfeuv  2021  mo23  2044  bm1.1  2139  nfnfc1  2299  nfnfc  2303  nfeq  2304  nfabdw  2315  sbcnestgf  3078  dfnfc2  3786  nfdisjv  3950  nfdisj1  3951  nffr  4304  exmidfodomrlemr  7116  exmidfodomrlemrALT  7117  exmidunben  12106  bdsepnft  13400  bdsepnfALT  13402  setindft  13478  strcollnft  13497  pw1nct  13514
 Copyright terms: Public domain W3C validator