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

Theorem nfbi 1459
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
nfbi.1 xφ
nfbi.2 xψ
Assertion
Ref Expression
nfbi x(φψ)

Proof of Theorem nfbi
StepHypRef Expression
1 nfbi.1 . . . 4 xφ
21a1i 9 . . 3 ( ⊤ → Ⅎxφ)
3 nfbi.2 . . . 4 xψ
43a1i 9 . . 3 ( ⊤ → Ⅎxψ)
52, 4nfbid 1458 . 2 ( ⊤ → Ⅎx(φψ))
65trud 1235 1 x(φψ)
Colors of variables: wff set class
Syntax hints:  wb 98  wtru 1227  wnf 1325
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 1312  ax-gen 1314  ax-4 1377  ax-ial 1405  ax-i5r 1406
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326
This theorem is referenced by:  sb8eu  1891  nfeuv  1896  bm1.1  2003  abbi  2129  nfeq  2163  cleqf  2179  sbhypf  2576  ceqsexg  2645  elabgt  2657  elabgf  2658  copsex2t  3952  copsex2g  3953  opelopabsb  3967  opeliunxp2  4399  ralxpf  4405  rexxpf  4406  cbviota  4795  sb8iota  4797  fmptco  5251  nfiso  5367  dfoprab4f  5738  bdsepnfALT  7254  strcollnfALT  7343
  Copyright terms: Public domain W3C validator