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  2051  nfeuv  2056  bm1.1  2174  abbi  2303  nfeq  2340  cleqf  2357  sbhypf  2801  ceqsexg  2880  elabgt  2893  elabgf  2894  copsex2t  4263  copsex2g  4264  opelopabsb  4278  opeliunxp2  4785  ralxpf  4791  rexxpf  4792  cbviota  5201  sb8iota  5203  fmptco  5703  nfiso  5828  dfoprab4f  6219  opeliunxp2f  6264  xpf1o  6873  bdsepnfALT  15119