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 1472 | . 2 ⊢ (∀𝑥𝜓 → 𝜓) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1314 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-4 1472 |
This theorem is referenced by: 19.21bbi 1523 ax11e 1752 eqeq1 2124 eleq2 2181 r19.21bi 2497 elrab3t 2812 ssel 3061 exmidsssn 4095 copsex2t 4137 pocl 4195 ordsucim 4386 peano2 4479 funmo 5108 funun 5137 fununi 5161 imain 5175 tfrlem3-2d 6177 tfr1onlemaccex 6213 tfri1dALT 6216 tfrcllemaccex 6226 findcard 6750 findcard2 6751 findcard2s 6752 exmidpw 6770 |
Copyright terms: Public domain | W3C validator |