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

Theorem nf5ri 2190
Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 15-Mar-2023.)
Hypothesis
Ref Expression
nf5ri.1 𝑥𝜑
Assertion
Ref Expression
nf5ri (𝜑 → ∀𝑥𝜑)

Proof of Theorem nf5ri
StepHypRef Expression
1 nf5ri.1 . . 3 𝑥𝜑
21nfri 1786 . 2 (∃𝑥𝜑 → ∀𝑥𝜑)
3219.23bi 2185 1 (𝜑 → ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1531  wnf 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2172
This theorem depends on definitions:  df-bi 209  df-ex 1777  df-nf 1781
This theorem is referenced by:  19.3  2197  alimd  2207  alrimi  2208  eximd  2211  nexd  2218  albid  2219  exbid  2220  hbs1  2270  sbbibOLD  2285  hba1  2297  hban  2304  hb3an  2305  nfal  2338  hbex  2340  hbsbw  2347  cbv3v  2351  cbv3  2411  cbv2OLD  2423  equs45f  2478  nfs1  2523  sb6f  2533  hbsb  2563  sb6fALT  2598  nfsab  2812  nfsabg  2813  nfcrii  2970  ralrimi  3216  hbra1  3220  bnj1316  32087  bnj1379  32097  bnj1468  32113  bnj958  32207  bnj981  32217  bnj1014  32228  bnj1128  32257  bnj1204  32279  bnj1279  32285  bnj1398  32301  bnj1408  32303  bnj1444  32310  bnj1445  32311  bnj1446  32312  bnj1447  32313  bnj1448  32314  bnj1449  32315  bnj1463  32322  bnj1312  32325  bnj1518  32331  bnj1519  32332  bnj1520  32333  bnj1525  32336  bj-cbv2v  34115  bj-equs45fv  34128  mpobi123f  35434
  Copyright terms: Public domain W3C validator