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

Theorem nfbi 1970
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 1969 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65trud 1630 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wtru 1621  wnf 1845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847
This theorem is referenced by:  euf  2603  sb8eu  2629  bm1.1  2733  cleqh  2850  sbhypf  3381  ceqsexg  3461  elabgt  3475  elabgf  3476  axrep1  4912  axrep3  4914  axrep4  4915  copsex2t  5093  copsex2g  5094  opelopabsb  5123  opeliunxp2  5404  ralxpf  5412  cbviota  6005  sb8iota  6007  fvopab5  6460  fmptco  6547  nfiso  6723  dfoprab4f  7381  opeliunxp2f  7493  xpf1o  8275  zfcndrep  9599  gsumcom2  18545  isfildlem  21833  cnextfvval  22041  mbfsup  23601  mbfinf  23602  brabgaf  29698  fmptcof2  29737  bnj1468  31194  subtr2  32586  bj-abbi  33052  bj-axrep1  33065  bj-axrep3  33067  bj-axrep4  33068  mpt2bi123f  34253  eqrelf  34313  fourierdlem31  40827
  Copyright terms: Public domain W3C validator