Theorem nfbi 1635

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

Syntax hints:   <-> wb 105   T. wtru 1396   F/wnf 1506

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 1493  ax-gen 1495  ax-4 1556  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507

This theorem is referenced by:  sb8eu  2090  nfeuv  2095  bm1.1  2214  abbi  2343  nfeq  2380  cleqf  2397  sbhypf  2850  ceqsexg  2931  elabgt  2944  elabgf  2945  copsex2t  4331  copsex2g  4332  opelopabsb  4348  opeliunxp2  4862  ralxpf  4868  rexxpf  4869  cbviota  5283  sb8iota  5286  fmptco  5801  nfiso  5930  uchoice  6283  dfoprab4f  6339  opeliunxp2f  6384  xpf1o  7005  bdsepnfALT  16252