Theorem nfbi 1903

Description: If 𝑥 is not free in 𝜑 and 𝜓, then 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

Step	Hyp	Ref	Expression
1		nf.1	. . . 4 ⊢ Ⅎ𝑥𝜑
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
3		nf.2	. . . 4 ⊢ Ⅎ𝑥𝜓
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜓)
5	2, 4	nfbid 1902	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓))
6	5	mptru 1547	1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 206  ⊤wtru 1541  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by:  sbbib  2363  euf  2575  sb8eulem  2597  axextmo  2711  abbib  2804  cleqh  2864  cleqf  2927  sbhypfOLD  3524  ceqsexg  3632  elabgf  3653  axrep1  5250  axrep3  5253  axrep4OLD  5256  copsex2t  5467  opeliunxp2  5818  ralxpf  5826  cbviotaw  6491  cbviota  6493  sb8iota  6495  fvopab5  7019  fmptco  7119  nfiso  7315  dfoprab4f  8055  opeliunxp2f  8209  xpf1o  9153  zfcndrep  10628  gsumcom2  19956  isfildlem  23795  cnextfvval  24003  mbfsup  25617  mbfinf  25618  brabgaf  32588  fmptcof2  32635  bnj1468  34877  subtr2  36333  mpobi123f  38186  eqrelf  38273  unielss  43242  permaxrep  45031  fourierdlem31  46167