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

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
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 1525 . 2  |-  ( T. 
->  F/ x ( ph  <->  ps ) )
65mptru 1298 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator