Theorem nfbi 1600

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 1599	. 2 |- ( T. -> F/ x ( ph <-> ps ) )
6	5	mptru 1373	1 |- F/ x ( ph <-> ps )

Syntax hints:   <-> wb 105   T. wtru 1365   F/wnf 1471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472

This theorem is referenced by:  sb8eu  2055  nfeuv  2060  bm1.1  2178  abbi  2307  nfeq  2344  cleqf  2361  sbhypf  2809  ceqsexg  2888  elabgt  2901  elabgf  2902  copsex2t  4274  copsex2g  4275  opelopabsb  4290  opeliunxp2  4802  ralxpf  4808  rexxpf  4809  cbviota  5220  sb8iota  5222  fmptco  5724  nfiso  5849  uchoice  6190  dfoprab4f  6246  opeliunxp2f  6291  xpf1o  6900  bdsepnfALT  15381