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

Theorem nfbi 1612
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 1611 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65mptru 1382 1 𝑥(𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wb 105  wtru 1374  wnf 1483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-4 1533  ax-ial 1557  ax-i5r 1558
This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484
This theorem is referenced by:  sb8eu  2067  nfeuv  2072  bm1.1  2190  abbi  2319  nfeq  2356  cleqf  2373  sbhypf  2822  ceqsexg  2901  elabgt  2914  elabgf  2915  copsex2t  4289  copsex2g  4290  opelopabsb  4306  opeliunxp2  4818  ralxpf  4824  rexxpf  4825  cbviota  5237  sb8iota  5239  fmptco  5746  nfiso  5875  uchoice  6223  dfoprab4f  6279  opeliunxp2f  6324  xpf1o  6941  bdsepnfALT  15825
  Copyright terms: Public domain W3C validator