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

Theorem nfbi 1549
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 1548 . 2  |-  ( T. 
->  F/ x ( ph  <->  ps ) )
65mptru 1321 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   T. wtru 1313   F/wnf 1417
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-4 1468  ax-ial 1495  ax-i5r 1496
This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418
This theorem is referenced by:  sb8eu  1986  nfeuv  1991  bm1.1  2098  abbi  2226  nfeq  2261  cleqf  2277  sbhypf  2704  ceqsexg  2781  elabgt  2793  elabgf  2794  copsex2t  4125  copsex2g  4126  opelopabsb  4140  opeliunxp2  4637  ralxpf  4643  rexxpf  4644  cbviota  5049  sb8iota  5051  fmptco  5538  nfiso  5659  dfoprab4f  6042  opeliunxp2f  6086  xpf1o  6688  bdsepnfALT  12766  strcollnfALT  12863
  Copyright terms: Public domain W3C validator