MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfbi Structured version   Visualization version   GIF version

Theorem nfbi 1903
Description: If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑𝜓). (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
Hypotheses
Ref Expression
nf.1 𝑥𝜑
nf.2 𝑥𝜓
Assertion
Ref Expression
nfbi 𝑥(𝜑𝜓)

Proof of Theorem nfbi
StepHypRef Expression
1 nf.1 . . . 4 𝑥𝜑
21a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
3 nf.2 . . . 4 𝑥𝜓
43a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜓)
52, 4nfbid 1902 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65mptru 1547 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wtru 1541  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784
This theorem is referenced by:  sbbib  2364  euf  2576  sb8eulem  2598  axextmo  2712  abbib  2811  cleqh  2871  cleqf  2934  sbhypfOLD  3545  ceqsexg  3653  elabgf  3674  axrep1  5280  axrep3  5283  axrep4OLD  5286  copsex2t  5497  opeliunxp2  5849  ralxpf  5857  cbviotaw  6521  cbviota  6523  sb8iota  6525  fvopab5  7049  fmptco  7149  nfiso  7342  dfoprab4f  8081  opeliunxp2f  8235  xpf1o  9179  zfcndrep  10654  gsumcom2  19993  isfildlem  23865  cnextfvval  24073  mbfsup  25699  mbfinf  25700  brabgaf  32620  fmptcof2  32667  bnj1468  34860  subtr2  36316  mpobi123f  38169  eqrelf  38256  unielss  43230  fourierdlem31  46153
  Copyright terms: Public domain W3C validator