**Description:** Deduction form of nfal . (Contributed by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 16-Oct-2021)

Ref | Expression | ||
---|---|---|---|

Hypotheses | nfald.1 | ⊢ Ⅎ 𝑦 𝜑 | |

nfald.2 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 ) | ||

Assertion | nfald | ⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 𝜓 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | nfald.1 | ⊢ Ⅎ 𝑦 𝜑 | |

2 | nfald.2 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 ) | |

3 | 19.12 | ⊢ ( ∃ 𝑥 ∀ 𝑦 𝜓 → ∀ 𝑦 ∃ 𝑥 𝜓 ) | |

4 | 2 | nfrd | ⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜓 ) ) |

5 | 1 4 | alimd | ⊢ ( 𝜑 → ( ∀ 𝑦 ∃ 𝑥 𝜓 → ∀ 𝑦 ∀ 𝑥 𝜓 ) ) |

6 | ax-11 | ⊢ ( ∀ 𝑦 ∀ 𝑥 𝜓 → ∀ 𝑥 ∀ 𝑦 𝜓 ) | |

7 | 3 5 6 | syl56 | ⊢ ( 𝜑 → ( ∃ 𝑥 ∀ 𝑦 𝜓 → ∀ 𝑥 ∀ 𝑦 𝜓 ) ) |

8 | 7 | nfd | ⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑦 𝜓 ) |