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

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

Proof of Theorem nfbi
StepHypRef Expression
1 nfbi.1 . . . 4
21a1i 9 . . 3
3 nfbi.2 . . . 4
43a1i 9 . . 3
52, 4nfbid 1480 . 2
65trud 1252 1
 Colors of variables: wff set class Syntax hints:   wb 98   wtru 1244  wnf 1349 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 1336  ax-gen 1338  ax-4 1400  ax-ial 1427  ax-i5r 1428 This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350 This theorem is referenced by:  sb8eu  1913  nfeuv  1918  bm1.1  2025  abbi  2151  nfeq  2185  cleqf  2201  sbhypf  2603  ceqsexg  2672  elabgt  2684  elabgf  2685  copsex2t  3982  copsex2g  3983  opelopabsb  3997  opeliunxp2  4476  ralxpf  4482  rexxpf  4483  cbviota  4872  sb8iota  4874  fmptco  5330  nfiso  5446  dfoprab4f  5819  bdsepnfALT  10009  strcollnfALT  10111
 Copyright terms: Public domain W3C validator