MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfri Unicode version

Theorem nfri 1742
Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfri.1  |-  F/ x ph
Assertion
Ref Expression
nfri  |-  ( ph  ->  A. x ph )

Proof of Theorem nfri
StepHypRef Expression
1 nfri.1 . 2  |-  F/ x ph
2 nfr 1741 . 2  |-  ( F/ x ph  ->  ( ph  ->  A. x ph )
)
31, 2ax-mp 8 1  |-  ( ph  ->  A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527   F/wnf 1531
This theorem is referenced by:  alimd  1744  alrimi  1745  eximd  1750  nexd  1751  albid  1752  exbid  1753  nfal  1766  19.3  1781  stdpc5  1793  equsal  1900  equs45f  1929  cbvald  1948  sb6f  1979  nfs1  1984  hbsb  2049  nfsab  2275  nfcrii  2412  bnj1316  28853  bnj1379  28863  bnj1468  28878  bnj958  28972  bnj981  28982  bnj1014  28992  bnj1128  29020  bnj1204  29042  bnj1279  29048  bnj1309  29052  bnj1398  29064  bnj1408  29066  bnj1444  29073  bnj1445  29074  bnj1446  29075  bnj1447  29076  bnj1448  29077  bnj1449  29078  bnj1463  29085  bnj1312  29088  bnj1518  29094  bnj1519  29095  bnj1520  29096  bnj1525  29099  a12lem1  29130
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator