Theorem nfbi 1603

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

Syntax hints:   <-> wb 105   T. wtru 1365   F/wnf 1474

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 1461  ax-gen 1463  ax-4 1524  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475

This theorem is referenced by:  sb8eu  2058  nfeuv  2063  bm1.1  2181  abbi  2310  nfeq  2347  cleqf  2364  sbhypf  2813  ceqsexg  2892  elabgt  2905  elabgf  2906  copsex2t  4278  copsex2g  4279  opelopabsb  4294  opeliunxp2  4806  ralxpf  4812  rexxpf  4813  cbviota  5224  sb8iota  5226  fmptco  5728  nfiso  5853  uchoice  6195  dfoprab4f  6251  opeliunxp2f  6296  xpf1o  6905  bdsepnfALT  15535