Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfbi Structured version   Visualization version   GIF version

Theorem nfbi 1821
 Description: If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ↔ 𝜓). (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
Hypotheses
Ref Expression
nf.1 𝑥𝜑
nf.2 𝑥𝜓
Assertion
Ref Expression
nfbi 𝑥(𝜑𝜓)

Proof of Theorem nfbi
StepHypRef Expression
1 nf.1 . . . 4 𝑥𝜑
21a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
3 nf.2 . . . 4 𝑥𝜓
43a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜓)
52, 4nfbid 1820 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65trud 1484 1 𝑥(𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195  ⊤wtru 1476  Ⅎwnf 1699 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701 This theorem is referenced by:  euf  2466  sb8eu  2491  bm1.1  2595  cleqh  2711  sbhypf  3226  ceqsexg  3304  elabgt  3316  elabgf  3317  axrep1  4700  axrep3  4702  axrep4  4703  copsex2t  4883  copsex2g  4884  opelopabsb  4910  opeliunxp2  5182  ralxpf  5190  cbviota  5773  sb8iota  5775  fvopab5  6217  fmptco  6303  nfiso  6472  dfoprab4f  7117  opeliunxp2f  7223  xpf1o  8007  zfcndrep  9315  gsumcom2  18197  isfildlem  21471  cnextfvval  21679  mbfsup  23237  mbfinf  23238  brabgaf  28800  fmptcof2  28839  bnj1468  30170  subtr2  31479  bj-abbi  31963  bj-axrep1  31976  bj-axrep3  31978  bj-axrep4  31979  mpt2bi123f  33141  dfcleqf  38281  fourierdlem31  39031
 Copyright terms: Public domain W3C validator