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

Theorem nfald 2164
 Description: Deduction form of nfal 2152. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.) (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 2163 . . 3 (∃𝑥𝑦𝜓 → ∀𝑦𝑥𝜓)
2 nfald.1 . . . 4 𝑦𝜑
3 nfald.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfrd 1716 . . . 4 (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
52, 4alimd 2080 . . 3 (𝜑 → (∀𝑦𝑥𝜓 → ∀𝑦𝑥𝜓))
6 ax-11 2033 . . 3 (∀𝑦𝑥𝜓 → ∀𝑥𝑦𝜓)
71, 5, 6syl56 36 . 2 (𝜑 → (∃𝑥𝑦𝜓 → ∀𝑥𝑦𝜓))
87nfd 1715 1 (𝜑 → Ⅎ𝑥𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1480  ∃wex 1703  Ⅎwnf 1707 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-10 2018  ax-11 2033  ax-12 2046 This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1704  df-nf 1709 This theorem is referenced by:  nfexd  2166  dvelimhw  2172  nfald2  2330  nfeqd  2771  axrepndlem1  9411  axrepndlem2  9412  axunnd  9415  axpowndlem2  9417  axpowndlem4  9419  axregndlem2  9422  axinfndlem1  9424  axinfnd  9425  axacndlem4  9429  axacndlem5  9430  axacnd  9431  bj-dvelimdv  32818  wl-mo2df  33332  wl-eudf  33334  wl-mo2t  33337  nfintd  42191
 Copyright terms: Public domain W3C validator