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  2787  ceqsexg  2866  elabgt  2879  elabgf  2880  copsex2t  4246  copsex2g  4247  opelopabsb  4261  opeliunxp2  4768  ralxpf  4774  rexxpf  4775  cbviota  5184  sb8iota  5186  fmptco  5683  nfiso  5807  dfoprab4f  6194  opeliunxp2f  6239  xpf1o  6844  bdsepnfALT  14644
  Copyright terms: Public domain W3C validator