![]() |
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 1445 | . 2 ⊢ (∀𝑥𝜓 → 𝜓) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1287 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-4 1445 |
This theorem is referenced by: 19.21bbi 1496 ax11e 1724 eqeq1 2094 eleq2 2151 r19.21bi 2461 elrab3t 2770 ssel 3019 copsex2t 4072 pocl 4130 ordsucim 4317 peano2 4410 funmo 5030 funun 5058 fununi 5082 imain 5096 tfrlem3-2d 6077 tfr1onlemaccex 6113 tfri1dALT 6116 tfrcllemaccex 6126 findcard 6602 findcard2 6603 findcard2s 6604 exmidpw 6622 |
Copyright terms: Public domain | W3C validator |