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

Theorem nfald 1977
Description: Deduction form of nfal 1973. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.)
Hypotheses
Ref Expression
nfald.1  |-  F/ y
ph
nfald.2  |-  ( ph  ->  F/ x ps )
Assertion
Ref Expression
nfald  |-  ( ph  ->  F/ x A. y ps )

Proof of Theorem nfald
StepHypRef Expression
1 nfald.1 . . 3  |-  F/ y
ph
2 nfald.2 . . 3  |-  ( ph  ->  F/ x ps )
31, 2alrimi 1899 . 2  |-  ( ph  ->  A. y F/ x ps )
4 nfnf1 1925 . . . 4  |-  F/ x F/ x ps
54nfal 1973 . . 3  |-  F/ x A. y F/ x ps
6 hba1 1922 . . . 4  |-  ( A. y F/ x ps  ->  A. y A. y F/ x ps )
7 sp 1881 . . . . 5  |-  ( A. y F/ x ps  ->  F/ x ps )
87nfrd 1897 . . . 4  |-  ( A. y F/ x ps  ->  ( ps  ->  A. x ps ) )
96, 8hbald 1870 . . 3  |-  ( A. y F/ x ps  ->  ( A. y ps  ->  A. x A. y ps ) )
105, 9nfd 1900 . 2  |-  ( A. y F/ x ps  ->  F/ x A. y ps )
113, 10syl 17 1  |-  ( ph  ->  F/ x A. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1401   F/wnf 1635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-10 1859  ax-11 1864  ax-12 1876
This theorem depends on definitions:  df-bi 185  df-ex 1632  df-nf 1636
This theorem is referenced by:  nfexd  1978  dvelimhw  1981  nfald2  2097  nfeqd  2569  axrepndlem1  8917  axrepndlem2  8918  axunnd  8921  axpowndlem2  8923  axpowndlem4  8925  axregndlem2  8928  axinfndlem1  8931  axinfnd  8932  axacndlem4  8936  axacndlem5  8937  axacnd  8938  wl-mo2dnae  31355  wl-mo2t  31356
  Copyright terms: Public domain W3C validator