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

Theorem nfbi 1909
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 1908 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65mptru 1549 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wtru 1543  wnf 1790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791
This theorem is referenced by:  sbbib  2361  euf  2577  sb8eulem  2599  axextmo  2714  abbi  2805  cleqh  2856  cleqf  2930  sbhypf  3455  ceqsexg  3547  elabgt  3565  elabgf  3566  elabg  3570  axrep1  5152  axrep3  5155  axrep4  5156  copsex2t  5346  copsex2gOLD  5348  opeliunxp2  5675  ralxpf  5683  cbviotaw  6298  cbviota  6301  sb8iota  6303  fvopab5  6801  fmptco  6895  nfiso  7082  dfoprab4f  7772  opeliunxp2f  7898  xpf1o  8722  zfcndrep  10107  gsumcom2  19207  isfildlem  22601  cnextfvval  22809  mbfsup  24409  mbfinf  24410  brabgaf  30514  fmptcof2  30561  bnj1468  32389  subtr2  34134  mpobi123f  35932  eqrelf  36007  fourierdlem31  43205
  Copyright terms: Public domain W3C validator