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

Theorem nfald 2328
Description: Deduction form of nfal 2323. (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 2327 . . 3 (∃𝑥𝑦𝜓 → ∀𝑦𝑥𝜓)
2 nfald.1 . . . 4 𝑦𝜑
3 nfald.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfrd 1791 . . . 4 (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))
52, 4alimd 2212 . . 3 (𝜑 → (∀𝑦𝑥𝜓 → ∀𝑦𝑥𝜓))
6 ax-11 2157 . . 3 (∀𝑦𝑥𝜓 → ∀𝑥𝑦𝜓)
71, 5, 6syl56 36 . 2 (𝜑 → (∃𝑥𝑦𝜓 → ∀𝑥𝑦𝜓))
87nfd 1790 1 (𝜑 → Ⅎ𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1538  wex 1779  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1780  df-nf 1784
This theorem is referenced by:  nfexd  2329  dvelimhw  2347  nfald2  2450  nfmodv  2559  nfeqd  2916  nfabdw  2927  nfraldw  3309  nfiotadw  6517  nfixpw  8956  axrepndlem1  10632  axrepndlem2  10633  axunnd  10636  axpowndlem2  10638  axpowndlem4  10640  axregndlem2  10643  axinfndlem1  10645  axinfnd  10646  axacndlem4  10650  axacndlem5  10651  axacnd  10652  axsepg2  35096  axsepg2ALT  35097  axnulg  35106  bj-dvelimdv  36852  wl-mo2df  37571  wl-eudf  37573  wl-mo2t  37576  nfintd  49192
  Copyright terms: Public domain W3C validator