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

Theorem nfbi 1611
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 1610 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65mptru 1381 1 𝑥(𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wb 105  wtru 1373  wnf 1482
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 1469  ax-gen 1471  ax-4 1532  ax-ial 1556  ax-i5r 1557
This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483
This theorem is referenced by:  sb8eu  2066  nfeuv  2071  bm1.1  2189  abbi  2318  nfeq  2355  cleqf  2372  sbhypf  2821  ceqsexg  2900  elabgt  2913  elabgf  2914  copsex2t  4288  copsex2g  4289  opelopabsb  4305  opeliunxp2  4817  ralxpf  4823  rexxpf  4824  cbviota  5236  sb8iota  5238  fmptco  5745  nfiso  5874  uchoice  6222  dfoprab4f  6278  opeliunxp2f  6323  xpf1o  6940  bdsepnfALT  15787
  Copyright terms: Public domain W3C validator