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

Theorem nfbi 1577
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 1576 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65mptru 1352 1 𝑥(𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wtru 1344  wnf 1448
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 1435  ax-gen 1437  ax-4 1498  ax-ial 1522  ax-i5r 1523
This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449
This theorem is referenced by:  sb8eu  2027  nfeuv  2032  bm1.1  2150  abbi  2280  nfeq  2316  cleqf  2333  sbhypf  2775  ceqsexg  2854  elabgt  2867  elabgf  2868  copsex2t  4223  copsex2g  4224  opelopabsb  4238  opeliunxp2  4744  ralxpf  4750  rexxpf  4751  cbviota  5158  sb8iota  5160  fmptco  5651  nfiso  5774  dfoprab4f  6161  opeliunxp2f  6206  xpf1o  6810  bdsepnfALT  13771
  Copyright terms: Public domain W3C validator