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

Theorem nfald 2317
Description: Deduction form of nfal 2312. (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 2316 . . 3 (∃𝑥𝑦𝜓 → ∀𝑦𝑥𝜓)
2 nfald.1 . . . 4 𝑦𝜑
3 nfald.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfrd 1786 . . . 4 (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
52, 4alimd 2201 . . 3 (𝜑 → (∀𝑦𝑥𝜓 → ∀𝑦𝑥𝜓))
6 ax-11 2147 . . 3 (∀𝑦𝑥𝜓 → ∀𝑥𝑦𝜓)
71, 5, 6syl56 36 . 2 (𝜑 → (∃𝑥𝑦𝜓 → ∀𝑥𝑦𝜓))
87nfd 1785 1 (𝜑 → Ⅎ𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1532  wex 1774  wnf 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-10 2130  ax-11 2147  ax-12 2167
This theorem depends on definitions:  df-bi 206  df-or 846  df-ex 1775  df-nf 1779
This theorem is referenced by:  nfexd  2318  dvelimhw  2336  nfald2  2439  nfmodv  2548  nfeqd  2903  nfabdw  2916  nfraldw  3297  nfraldwOLD  3309  nfiotadw  6501  nfixpw  8937  axrepndlem1  10626  axrepndlem2  10627  axunnd  10630  axpowndlem2  10632  axpowndlem4  10634  axregndlem2  10637  axinfndlem1  10639  axinfnd  10640  axacndlem4  10644  axacndlem5  10645  axacnd  10646  bj-dvelimdv  36569  wl-mo2df  37278  wl-eudf  37280  wl-mo2t  37283  nfintd  48455
  Copyright terms: Public domain W3C validator