Theorem nfbi 1478

Description: If x is not free in ph and ps, 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/xph
nfbi.2	|- F/xps

Assertion

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

Proof of Theorem nfbi

Step	Hyp	Ref	Expression
1		nfbi.1	. . . 4 |- F/xph
2	1	a1i 9	. . 3 |- ( T. -> F/xph)
3		nfbi.2	. . . 4 |- F/xps
4	3	a1i 9	. . 3 |- ( T. -> F/xps)
5	2, 4	nfbid 1477	. 2 |- ( T. -> F/x(ph <-> ps))
6	5	trud 1251	1 |- F/x(ph <-> ps)

Syntax hints:   <-> wb 98   T. wtru 1243   F/wnf 1346

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-ial 1424  ax-i5r 1425

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347

This theorem is referenced by:  sb8eu  1910  nfeuv  1915  bm1.1  2022  abbi  2148  nfeq  2182  cleqf  2198  sbhypf  2597  ceqsexg  2666  elabgt  2678  elabgf  2679  copsex2t  3973  copsex2g  3974  opelopabsb  3988  opeliunxp2  4419  ralxpf  4425  rexxpf  4426  cbviota  4815  sb8iota  4817  fmptco  5273  nfiso  5389  dfoprab4f  5761  bdsepnfALT  9323  strcollnfALT  9416