![]() |
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 1441 | . 2 ⊢ (∀𝑥𝜓 → 𝜓) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1283 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-4 1441 |
This theorem is referenced by: 19.21bbi 1492 ax11e 1719 eqeq1 2089 eleq2 2146 r19.21bi 2454 elrab3t 2756 ssel 3002 copsex2t 4028 pocl 4086 ordsucim 4272 peano2 4364 funmo 4967 funun 4994 fununi 5018 imain 5032 tfrlem3-2d 5981 tfr1onlemaccex 6017 tfri1dALT 6020 tfrcllemaccex 6030 findcard 6444 findcard2 6445 findcard2s 6446 |
Copyright terms: Public domain | W3C validator |