Theorem nfbi 1576

Description: If x is not free in ph and ps, then it is not free in ( ph <-> ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)

Hypotheses

Ref	Expression
nfbi.1	|- F/ x ph
nfbi.2	|- F/ x ps

Assertion

Ref	Expression
nfbi	|- F/ x ( ph <-> ps )

Proof of Theorem nfbi

Step	Hyp	Ref	Expression
1		nfbi.1	. . . 4 |- F/ x ph
2	1	a1i 9	. . 3 |- ( T. -> F/ x ph )
3		nfbi.2	. . . 4 |- F/ x ps
4	3	a1i 9	. . 3 |- ( T. -> F/ x ps )
5	2, 4	nfbid 1575	. 2 |- ( T. -> F/ x ( ph <-> ps ) )
6	5	mptru 1351	1 |- F/ x ( ph <-> ps )

Syntax hints:   <-> wb 104   T. wtru 1343   F/wnf 1447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-4 1497  ax-ial 1521  ax-i5r 1522

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448

This theorem is referenced by:  sb8eu  2026  nfeuv  2031  bm1.1  2149  abbi  2278  nfeq  2314  cleqf  2331  sbhypf  2770  ceqsexg  2849  elabgt  2862  elabgf  2863  copsex2t  4217  copsex2g  4218  opelopabsb  4232  opeliunxp2  4738  ralxpf  4744  rexxpf  4745  cbviota  5152  sb8iota  5154  fmptco  5645  nfiso  5768  dfoprab4f  6153  opeliunxp2f  6197  xpf1o  6801  bdsepnfALT  13606