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

Theorem nfbi 1873
 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 1872 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65trud 1533 1 𝑥(𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196  ⊤wtru 1524  Ⅎwnf 1748 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750 This theorem is referenced by:  euf  2506  sb8eu  2532  bm1.1  2636  cleqh  2753  sbhypf  3284  ceqsexg  3365  elabgt  3379  elabgf  3380  axrep1  4805  axrep3  4807  axrep4  4808  copsex2t  4986  copsex2g  4987  opelopabsb  5014  opeliunxp2  5293  ralxpf  5301  cbviota  5894  sb8iota  5896  fvopab5  6349  fmptco  6436  nfiso  6612  dfoprab4f  7270  opeliunxp2f  7381  xpf1o  8163  zfcndrep  9474  gsumcom2  18420  isfildlem  21708  cnextfvval  21916  mbfsup  23476  mbfinf  23477  brabgaf  29546  fmptcof2  29585  bnj1468  31042  subtr2  32434  bj-abbi  32900  bj-axrep1  32913  bj-axrep3  32915  bj-axrep4  32916  mpt2bi123f  34101  eqrelf  34161  fourierdlem31  40673
 Copyright terms: Public domain W3C validator