Theorem nfbi 1577

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

Syntax hints:   <-> wb 104   T. wtru 1344   F/wnf 1448

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 1435  ax-gen 1437  ax-4 1498  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449

This theorem is referenced by:  sb8eu  2027  nfeuv  2032  bm1.1  2150  abbi  2280  nfeq  2316  cleqf  2333  sbhypf  2775  ceqsexg  2854  elabgt  2867  elabgf  2868  copsex2t  4223  copsex2g  4224  opelopabsb  4238  opeliunxp2  4744  ralxpf  4750  rexxpf  4751  cbviota  5158  sb8iota  5160  fmptco  5651  nfiso  5774  dfoprab4f  6161  opeliunxp2f  6206  xpf1o  6810  bdsepnfALT  13771