![]() |
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 1510 | . 2 ⊢ (∀𝑥𝜓 → 𝜓) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1351 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-4 1510 |
This theorem is referenced by: 19.21bbi 1559 ax11e 1796 eqeq1 2184 eleq2 2241 r19.21bi 2565 elrab3t 2893 ssel 3150 exmidsssn 4203 copsex2t 4246 pocl 4304 ordsucim 4500 peano2 4595 funmo 5232 funun 5261 fununi 5285 imain 5299 tfrlem3-2d 6313 tfr1onlemaccex 6349 tfri1dALT 6352 tfrcllemaccex 6362 findcard 6888 findcard2 6889 findcard2s 6890 exmidpw 6908 exmidpweq 6909 |
Copyright terms: Public domain | W3C validator |