ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfbi Unicode version

Theorem nfbi 1522
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
StepHypRef Expression
1 nfbi.1 . . . 4  |-  F/ x ph
21a1i 9 . . 3  |-  ( T. 
->  F/ x ph )
3 nfbi.2 . . . 4  |-  F/ x ps
43a1i 9 . . 3  |-  ( T. 
->  F/ x ps )
52, 4nfbid 1521 . 2  |-  ( T. 
->  F/ x ( ph  <->  ps ) )
65trud 1294 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   T. wtru 1286   F/wnf 1390
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 1377  ax-gen 1379  ax-4 1441  ax-ial 1468  ax-i5r 1469
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391
This theorem is referenced by:  sb8eu  1956  nfeuv  1961  bm1.1  2068  abbi  2196  nfeq  2230  cleqf  2246  sbhypf  2657  ceqsexg  2732  elabgt  2744  elabgf  2745  copsex2t  4029  copsex2g  4030  opelopabsb  4044  opeliunxp2  4525  ralxpf  4531  rexxpf  4532  cbviota  4923  sb8iota  4925  fmptco  5383  nfiso  5498  dfoprab4f  5871  xpf1o  6407  bdsepnfALT  10931  strcollnfALT  11032
  Copyright terms: Public domain W3C validator