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

Theorem nfbi 1589
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 1588 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65mptru 1362 1 𝑥(𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wb 105  wtru 1354  wnf 1460
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 1447  ax-gen 1449  ax-4 1510  ax-ial 1534  ax-i5r 1535
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461
This theorem is referenced by:  sb8eu  2039  nfeuv  2044  bm1.1  2162  abbi  2291  nfeq  2327  cleqf  2344  sbhypf  2786  ceqsexg  2865  elabgt  2878  elabgf  2879  copsex2t  4245  copsex2g  4246  opelopabsb  4260  opeliunxp2  4767  ralxpf  4773  rexxpf  4774  cbviota  5183  sb8iota  5185  fmptco  5682  nfiso  5806  dfoprab4f  6193  opeliunxp2f  6238  xpf1o  6843  bdsepnfALT  14611
  Copyright terms: Public domain W3C validator