![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 19.21bi | GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
19.21bi.1 | ⊢ (𝜑 → ∀𝑥𝜓) |
Ref | Expression |
---|---|
19.21bi | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.21bi.1 | . 2 ⊢ (𝜑 → ∀𝑥𝜓) | |
2 | ax-4 1521 | . 2 ⊢ (∀𝑥𝜓 → 𝜓) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1362 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-4 1521 |
This theorem is referenced by: 19.21bbi 1570 ax11e 1807 eqeq1 2196 eleq2 2253 r19.21bi 2578 elrab3t 2907 ssel 3164 exmidsssn 4220 copsex2t 4263 pocl 4321 ordsucim 4517 peano2 4612 funmo 5250 funun 5279 fununi 5303 imain 5317 tfrlem3-2d 6338 tfr1onlemaccex 6374 tfri1dALT 6377 tfrcllemaccex 6387 findcard 6917 findcard2 6918 findcard2s 6919 exmidpw 6937 exmidpweq 6938 |
Copyright terms: Public domain | W3C validator |