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

Theorem nfbi 1600
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 1599 . 2  |-  ( T. 
->  F/ x ( ph  <->  ps ) )
65mptru 1373 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 105   T. wtru 1365   F/wnf 1471
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 1458  ax-gen 1460  ax-4 1521  ax-ial 1545  ax-i5r 1546
This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472
This theorem is referenced by:  sb8eu  2051  nfeuv  2056  bm1.1  2174  abbi  2303  nfeq  2340  cleqf  2357  sbhypf  2801  ceqsexg  2880  elabgt  2893  elabgf  2894  copsex2t  4263  copsex2g  4264  opelopabsb  4278  opeliunxp2  4785  ralxpf  4791  rexxpf  4792  cbviota  5201  sb8iota  5203  fmptco  5703  nfiso  5828  dfoprab4f  6219  opeliunxp2f  6264  xpf1o  6873  bdsepnfALT  15119
  Copyright terms: Public domain W3C validator