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

Theorem nfbi 1834
Description: If x 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
nf.1 xφ
nf.2 xψ
Assertion
Ref Expression
nfbi x(φψ)

Proof of Theorem nfbi
StepHypRef Expression
1 nf.1 . . . 4 xφ
21a1i 10 . . 3 ( ⊤ → Ⅎxφ)
3 nf.2 . . . 4 xψ
43a1i 10 . . 3 ( ⊤ → Ⅎxψ)
52, 4nfbid 1832 . 2 ( ⊤ → Ⅎx(φψ))
65trud 1323 1 x(φψ)
Colors of variables: wff setvar class
Syntax hints:  wb 176  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:  euf  2210  sb8eu  2222  bm1.1  2338  abbi  2463  nfeq  2496  cleqf  2513  sbhypf  2904  ceqsexg  2970  elabgt  2982  elabgf  2983  cbviota  4344  sb8iota  4346  copsex2t  4608  copsex2g  4609  opelopabsb  4697  opeliunxp2  4822  ralxpf  4827  nfiso  5487
  Copyright terms: Public domain W3C validator