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 2200 and also deduction form of sp 2176. (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 2176 | . 2 ⊢ (∀𝑥𝜓 → 𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1537 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: 19.21bbi 2183 axc7e 2312 eleq2w2 2734 eqeq1dALT 2741 eleq2dALT 2825 nfeqd 2917 sselOLD 3915 poclOLD 5511 funmo 6450 funun 6480 fununi 6509 findcard 8946 findcard2 8947 ssfi 8956 findcard2OLD 9056 ttrclselem2 9484 axpowndlem4 10356 axregndlem2 10359 axinfnd 10362 prcdnq 10749 dfrtrcl2 14773 relexpindlem 14774 bnj1379 32810 bnj1052 32955 bnj1118 32964 bnj1154 32979 bnj1280 33000 dftrcl3 41328 dfrtrcl3 41341 vk15.4j 42148 hbimpg 42174 |
Copyright terms: Public domain | W3C validator |