Theorem nfbi 1481

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/ 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 1480	. 2 |- ( T. -> F/ x ( ph <-> ps ) )
6	5	trud 1252	1 |- F/ x ( ph <-> ps )

Syntax hints:   <-> wb 98   T. wtru 1244   F/wnf 1349

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 1336  ax-gen 1338  ax-4 1400  ax-ial 1427  ax-i5r 1428

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350

This theorem is referenced by:  sb8eu  1913  nfeuv  1918  bm1.1  2025  abbi  2151  nfeq  2185  cleqf  2201  sbhypf  2603  ceqsexg  2672  elabgt  2684  elabgf  2685  copsex2t  3982  copsex2g  3983  opelopabsb  3997  opeliunxp2  4476  ralxpf  4482  rexxpf  4483  cbviota  4872  sb8iota  4874  fmptco  5330  nfiso  5446  dfoprab4f  5819  bdsepnfALT  10009  strcollnfALT  10111