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

Theorem nfald 2362
Description: Deduction form of nfal 2357. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 16-Oct-2021.)
Hypotheses
Ref Expression
nfald.1 𝑦𝜑
nfald.2 (𝜑 → Ⅎ𝑥𝜓)
Assertion
Ref Expression
nfald (𝜑 → Ⅎ𝑥𝑦𝜓)

Proof of Theorem nfald
StepHypRef Expression
1 19.12 2361 . . 3 (∃𝑥𝑦𝜓 → ∀𝑦𝑥𝜓)
2 nfald.1 . . . 4 𝑦𝜑
3 nfald.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfrd 1892 . . . 4 (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
52, 4alimd 2257 . . 3 (𝜑 → (∀𝑦𝑥𝜓 → ∀𝑦𝑥𝜓))
6 ax-11 2209 . . 3 (∀𝑦𝑥𝜓 → ∀𝑥𝑦𝜓)
71, 5, 6syl56 36 . 2 (𝜑 → (∃𝑥𝑦𝜓 → ∀𝑥𝑦𝜓))
87nfd 1891 1 (𝜑 → Ⅎ𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1656  wex 1880  wnf 1884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-10 2194  ax-11 2209  ax-12 2222
This theorem depends on definitions:  df-bi 199  df-or 881  df-ex 1881  df-nf 1885
This theorem is referenced by:  nfexd  2363  dvelimhw  2371  nfald2  2466  nfmodv  2628  nfeqd  2977  axrepndlem1  9729  axrepndlem2  9730  axunnd  9733  axpowndlem2  9735  axpowndlem4  9737  axregndlem2  9740  axinfndlem1  9742  axinfnd  9743  axacndlem4  9747  axacndlem5  9748  axacnd  9749  bj-dvelimdv  33357  wl-mo2df  33896  wl-eudf  33898  wl-mo2t  33901  nfintd  43315
  Copyright terms: Public domain W3C validator