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

Theorem nfri 1766
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 1765 . 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 1531   F/wnf 1535
This theorem is referenced by:  alimd  1768  alrimi  1769  eximd  1774  nexd  1775  albid  1776  exbid  1777  nfal  1794  nfex  1795  19.3  1810  19.9  1813  stdpc5  1824  equsal  1932  equs45f  1961  cbvald  1980  sb6f  2011  nfs1  2016  hbsb  2082  nfsab  2308  nfcrii  2445  bnj1316  28364  bnj1379  28374  bnj1468  28389  bnj958  28483  bnj981  28493  bnj1014  28503  bnj1128  28531  bnj1204  28553  bnj1279  28559  bnj1309  28563  bnj1398  28575  bnj1408  28577  bnj1444  28584  bnj1445  28585  bnj1446  28586  bnj1447  28587  bnj1448  28588  bnj1449  28589  bnj1463  28596  bnj1312  28599  bnj1518  28605  bnj1519  28606  bnj1520  28607  bnj1525  28610  nfalwAUX7  28622  equsalNEW7  28659  nfs1NEW7  28715  equs45fNEW7  28788  sb6fNEW7  28800  ax7nfAUX7  28821  nfalOLD7  28837  cbvaldOLD7  28884  hbsbOLD7  28899  a12lem1  28948
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-11 1732
This theorem depends on definitions:  df-bi 177  df-ex 1533  df-nf 1536
  Copyright terms: Public domain W3C validator