| 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 2207 and also deduction form of sp 2183. (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 2183 | . 2 ⊢ (∀𝑥𝜓 → 𝜓) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 |
| 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-12 2177 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: 19.21bbi 2190 axc7e 2318 eleq2w2 2733 eqeq1dALT 2740 eleq2dALT 2828 nfeqd 2916 funmoOLD 6582 funun 6612 fununi 6641 findcard 9203 findcard2 9204 ssfi 9213 ttrclselem2 9766 axpowndlem4 10640 axregndlem2 10643 axinfnd 10646 prcdnq 11033 dfrtrcl2 15101 relexpindlem 15102 bnj1379 34844 bnj1052 34989 bnj1118 34998 bnj1154 35013 bnj1280 35034 gblacfnacd 35113 dftrcl3 43733 dfrtrcl3 43746 vk15.4j 44548 hbimpg 44574 pgindnf 49235 |
| Copyright terms: Public domain | W3C validator |