![]() |
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 2201 and also deduction form of sp 2177. (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 2177 | . 2 ⊢ (∀𝑥𝜓 → 𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 |
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 1914 ax-6 1972 ax-7 2012 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: 19.21bbi 2184 axc7e 2312 eleq2w2 2729 eqeq1dALT 2736 eleq2dALT 2821 nfeqd 2914 sselOLD 3974 poclOLD 5592 funmoOLD 6556 funun 6586 fununi 6615 findcard 9151 findcard2 9152 ssfi 9161 findcard2OLD 9272 ttrclselem2 9708 axpowndlem4 10582 axregndlem2 10585 axinfnd 10588 prcdnq 10975 dfrtrcl2 14996 relexpindlem 14997 bnj1379 33772 bnj1052 33917 bnj1118 33926 bnj1154 33941 bnj1280 33962 dftrcl3 42342 dfrtrcl3 42355 vk15.4j 43160 hbimpg 43186 pgindnf 47601 |
Copyright terms: Public domain | W3C validator |