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

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
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 1567 . 2  |-  ( T. 
->  F/ x ( ph  <->  ps ) )
65mptru 1340 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff set class
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  4170  copsex2g  4171  opelopabsb  4185  opeliunxp2  4682  ralxpf  4688  rexxpf  4689  cbviota  5096  sb8iota  5098  fmptco  5589  nfiso  5710  dfoprab4f  6094  opeliunxp2f  6138  xpf1o  6741  bdsepnfALT  13231  strcollnfALT  13328
  Copyright terms: Public domain W3C validator