Theorem nfbi 1568

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

Syntax hints:   <-> wb 104   T. wtru 1332   F/wnf 1436

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 1423  ax-gen 1425  ax-4 1487  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437

This theorem is referenced by:  sb8eu  2012  nfeuv  2017  bm1.1  2124  abbi  2253  nfeq  2289  cleqf  2305  sbhypf  2735  ceqsexg  2813  elabgt  2825  elabgf  2826  copsex2t  4167  copsex2g  4168  opelopabsb  4182  opeliunxp2  4679  ralxpf  4685  rexxpf  4686  cbviota  5093  sb8iota  5095  fmptco  5586  nfiso  5707  dfoprab4f  6091  opeliunxp2f  6135  xpf1o  6738  bdsepnfALT  13087  strcollnfALT  13184