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

Theorem nfbi 1830
Description: If 𝑥 is not free in 𝜑 and 𝜓, 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 1829 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65trud 1490 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wtru 1481  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707
This theorem is referenced by:  euf  2477  sb8eu  2502  bm1.1  2606  cleqh  2721  sbhypf  3243  ceqsexg  3322  elabgt  3335  elabgf  3336  axrep1  4742  axrep3  4744  axrep4  4745  copsex2t  4927  copsex2g  4928  opelopabsb  4955  opeliunxp2  5230  ralxpf  5238  cbviota  5825  sb8iota  5827  fvopab5  6275  fmptco  6362  nfiso  6537  dfoprab4f  7186  opeliunxp2f  7296  xpf1o  8082  zfcndrep  9396  gsumcom2  18314  isfildlem  21601  cnextfvval  21809  mbfsup  23371  mbfinf  23372  brabgaf  29304  fmptcof2  29340  bnj1468  30677  subtr2  32004  bj-abbi  32471  bj-axrep1  32484  bj-axrep3  32486  bj-axrep4  32487  mpt2bi123f  33642  fourierdlem31  39692
  Copyright terms: Public domain W3C validator