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

Theorem nfbi 1553
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 1552 . 2  |-  ( T. 
->  F/ x ( ph  <->  ps ) )
65mptru 1325 1  |-  F/ x
( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   T. wtru 1317   F/wnf 1421
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 1408  ax-gen 1410  ax-4 1472  ax-ial 1499  ax-i5r 1500
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422
This theorem is referenced by:  sb8eu  1990  nfeuv  1995  bm1.1  2102  abbi  2231  nfeq  2266  cleqf  2282  sbhypf  2709  ceqsexg  2787  elabgt  2799  elabgf  2800  copsex2t  4137  copsex2g  4138  opelopabsb  4152  opeliunxp2  4649  ralxpf  4655  rexxpf  4656  cbviota  5063  sb8iota  5065  fmptco  5554  nfiso  5675  dfoprab4f  6059  opeliunxp2f  6103  xpf1o  6706  bdsepnfALT  13014  strcollnfALT  13111
  Copyright terms: Public domain W3C validator