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

Theorem nfald 2348
Description: Deduction form of nfal 2343. (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 2347 . . 3 (∃𝑥𝑦𝜓 → ∀𝑦𝑥𝜓)
2 nfald.1 . . . 4 𝑦𝜑
3 nfald.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfrd 1793 . . . 4 (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
52, 4alimd 2213 . . 3 (𝜑 → (∀𝑦𝑥𝜓 → ∀𝑦𝑥𝜓))
6 ax-11 2162 . . 3 (∀𝑦𝑥𝜓 → ∀𝑥𝑦𝜓)
71, 5, 6syl56 36 . 2 (𝜑 → (∃𝑥𝑦𝜓 → ∀𝑥𝑦𝜓))
87nfd 1792 1 (𝜑 → Ⅎ𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536  wex 1781  wnf 1785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-10 2146  ax-11 2162  ax-12 2178
This theorem depends on definitions:  df-bi 210  df-or 845  df-ex 1782  df-nf 1786
This theorem is referenced by:  nfexd  2349  dvelimhw  2367  nfald2  2468  nfmodv  2643  nfeqd  2984  nfraldw  3211  nfiotadw  6290  nfixpw  8455  axrepndlem1  9991  axrepndlem2  9992  axunnd  9995  axpowndlem2  9997  axpowndlem4  9999  axregndlem2  10002  axinfndlem1  10004  axinfnd  10005  axacndlem4  10009  axacndlem5  10010  axacnd  10011  bj-dvelimdv  34182  wl-mo2df  34849  wl-eudf  34851  wl-mo2t  34854  nfintd  44963
  Copyright terms: Public domain W3C validator