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  2359  euf  2569  sb8eulem  2591  axextmo  2705  abbib  2798  cleqh  2857  cleqf  2920  sbhypfOLD  3508  ceqsexg  3616  elabgf  3638  axrep1  5230  axrep3  5233  axrep4OLD  5236  copsex2t  5447  opeliunxp2  5792  ralxpf  5800  cbviotaw  6459  cbviota  6461  sb8iota  6463  fvopab5  6983  fmptco  7083  nfiso  7279  dfoprab4f  8014  opeliunxp2f  8166  xpf1o  9080  zfcndrep  10543  gsumcom2  19881  isfildlem  23720  cnextfvval  23928  mbfsup  25541  mbfinf  25542  brabgaf  32509  fmptcof2  32554  bnj1468  34809  subtr2  36276  mpobi123f  38129  eqrelf  38217  unielss  43180  permaxrep  44969  fourierdlem31  46109