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 2197 and also deduction form of sp 2172. (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 2172 | . 2 ⊢ (∀𝑥𝜓 → 𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: 19.21bbi 2179 axc7e 2328 eqeq1dALT 2821 eleq2dALT 2896 ssel 3958 pocl 5474 funmo 6364 funun 6393 fununi 6422 findcard 8745 findcard2 8746 axpowndlem4 10010 axregndlem2 10013 axinfnd 10016 prcdnq 10403 dfrtrcl2 14409 relexpindlem 14410 bnj1379 32001 bnj1052 32144 bnj1118 32153 bnj1154 32168 bnj1280 32189 dftrcl3 39943 dfrtrcl3 39956 vk15.4j 40739 hbimpg 40765 |
Copyright terms: Public domain | W3C validator |