Theorem nfbi 1526

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

Syntax hints:   <-> wb 103   T. wtru 1290   F/wnf 1394

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-ial 1472  ax-i5r 1473

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395

This theorem is referenced by:  sb8eu  1961  nfeuv  1966  bm1.1  2073  abbi  2201  nfeq  2236  cleqf  2252  sbhypf  2668  ceqsexg  2743  elabgt  2755  elabgf  2756  copsex2t  4063  copsex2g  4064  opelopabsb  4078  opeliunxp2  4564  ralxpf  4570  rexxpf  4571  cbviota  4972  sb8iota  4974  fmptco  5448  nfiso  5567  dfoprab4f  5945  opeliunxp2f  5985  xpf1o  6540  bdsepnfALT  11426  strcollnfALT  11527