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 1400 | . 2 ⊢ (∀𝑥𝜓 → 𝜓) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1241 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-4 1400 |
This theorem is referenced by: 19.21bbi 1451 ax11e 1677 eqeq1 2046 eleq2 2101 r19.21bi 2407 elrab3t 2697 ssel 2939 copsex2t 3982 pocl 4040 ordsucim 4226 peano2 4318 funmo 4917 funun 4944 fununi 4967 imain 4981 tfrlem3-2d 5928 findcard 6345 findcard2 6346 findcard2s 6347 |
Copyright terms: Public domain | W3C validator |