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

Theorem nfbi 1497
 Description: If 𝑥 is not free in 𝜑 and 𝜓, 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 1496 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65trud 1268 1 𝑥(𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   ↔ wb 102  ⊤wtru 1260  Ⅎwnf 1365 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-ial 1443  ax-i5r 1444 This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366 This theorem is referenced by:  sb8eu  1929  nfeuv  1934  bm1.1  2041  abbi  2167  nfeq  2201  cleqf  2217  sbhypf  2620  ceqsexg  2695  elabgt  2707  elabgf  2708  copsex2t  4010  copsex2g  4011  opelopabsb  4025  opeliunxp2  4504  ralxpf  4510  rexxpf  4511  cbviota  4900  sb8iota  4902  fmptco  5358  nfiso  5474  dfoprab4f  5847  bdsepnfALT  10396  strcollnfALT  10498
 Copyright terms: Public domain W3C validator