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

Theorem nfbi 1582
Description: If 𝑥 is not free in 𝜑 and 𝜓, then 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 1581 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65mptru 1357 1 𝑥(𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wtru 1349  wnf 1453
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 1440  ax-gen 1442  ax-4 1503  ax-ial 1527  ax-i5r 1528
This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454
This theorem is referenced by:  sb8eu  2032  nfeuv  2037  bm1.1  2155  abbi  2284  nfeq  2320  cleqf  2337  sbhypf  2779  ceqsexg  2858  elabgt  2871  elabgf  2872  copsex2t  4228  copsex2g  4229  opelopabsb  4243  opeliunxp2  4749  ralxpf  4755  rexxpf  4756  cbviota  5163  sb8iota  5165  fmptco  5659  nfiso  5782  dfoprab4f  6169  opeliunxp2f  6214  xpf1o  6818  bdsepnfALT  13884
  Copyright terms: Public domain W3C validator