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

Theorem nfald 2011
Description: Deduction form of nfal 2007. (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 1932 . 2  |-  ( ph  ->  A. y F/ x ps )
4 nfnf1 1958 . . . 4  |-  F/ x F/ x ps
54nfal 2007 . . 3  |-  F/ x A. y F/ x ps
6 hba1 1955 . . . 4  |-  ( A. y F/ x ps  ->  A. y A. y F/ x ps )
7 sp 1914 . . . . 5  |-  ( A. y F/ x ps  ->  F/ x ps )
87nfrd 1930 . . . 4  |-  ( A. y F/ x ps  ->  ( ps  ->  A. x ps ) )
96, 8hbald 1902 . . 3  |-  ( A. y F/ x ps  ->  ( A. y ps  ->  A. x A. y ps ) )
105, 9nfd 1933 . 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 1435   F/wnf 1661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909
This theorem depends on definitions:  df-bi 188  df-ex 1658  df-nf 1662
This theorem is referenced by:  nfexd  2012  dvelimhw  2015  nfald2  2132  nfeqd  2587  axrepndlem1  9024  axrepndlem2  9025  axunnd  9028  axpowndlem2  9030  axpowndlem4  9032  axregndlem2  9035  axinfndlem1  9037  axinfnd  9038  axacndlem4  9042  axacndlem5  9043  axacnd  9044  wl-mo2df  31863  wl-eudf  31865  wl-mo2t  31868
  Copyright terms: Public domain W3C validator