![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.21bi | Structured version Visualization version GIF version |
Description: Inference form of 19.21 2231 and also deduction form of sp 2207. (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
19.21bi.1 | ⊢ (𝜑 → ∀𝑥𝜓) |
Ref | Expression |
---|---|
19.21bi | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.21bi.1 | . 2 ⊢ (𝜑 → ∀𝑥𝜓) | |
2 | sp 2207 | . 2 ⊢ (∀𝑥𝜓 → 𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1629 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-12 2203 |
This theorem depends on definitions: df-bi 197 df-ex 1853 |
This theorem is referenced by: 19.21bbi 2214 axc7e 2297 eqeq1dALT 2774 eleq2dALT 2837 ssel 3746 pocl 5177 funmo 6047 funun 6075 fununi 6104 findcard 8355 findcard2 8356 axpowndlem4 9624 axregndlem2 9627 axinfnd 9630 prcdnq 10017 dfrtrcl2 14010 relexpindlem 14011 bnj1379 31239 bnj1052 31381 bnj1118 31390 bnj1154 31405 bnj1280 31426 dftrcl3 38538 dfrtrcl3 38551 vk15.4j 39259 hbimpg 39295 |
Copyright terms: Public domain | W3C validator |