Theorem nfbi 1589

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

Syntax hints:   <-> wb 105   T. wtru 1354   F/wnf 1460

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 1447  ax-gen 1449  ax-4 1510  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461

This theorem is referenced by:  sb8eu  2039  nfeuv  2044  bm1.1  2162  abbi  2291  nfeq  2327  cleqf  2344  sbhypf  2788  ceqsexg  2867  elabgt  2880  elabgf  2881  copsex2t  4247  copsex2g  4248  opelopabsb  4262  opeliunxp2  4769  ralxpf  4775  rexxpf  4776  cbviota  5185  sb8iota  5187  fmptco  5684  nfiso  5809  dfoprab4f  6196  opeliunxp2f  6241  xpf1o  6846  bdsepnfALT  14726