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 2209 and also deduction form of sp 2184. (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 2184 | . 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 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-12 2179 |
This theorem depends on definitions: df-bi 210 df-ex 1787 |
This theorem is referenced by: 19.21bbi 2191 axc7e 2320 eleq2w2 2734 eqeq1dALT 2741 eleq2dALT 2819 nfeqd 2909 sselOLD 3871 poclOLD 5450 funmo 6355 funun 6385 fununi 6414 findcard 8762 findcard2 8763 ssfi 8772 findcard2OLD 8834 axpowndlem4 10100 axregndlem2 10103 axinfnd 10106 prcdnq 10493 dfrtrcl2 14511 relexpindlem 14512 bnj1379 32381 bnj1052 32526 bnj1118 32535 bnj1154 32550 bnj1280 32571 dftrcl3 40874 dfrtrcl3 40887 vk15.4j 41686 hbimpg 41712 |
Copyright terms: Public domain | W3C validator |