Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > alrimih | Structured version Visualization version GIF version |
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2062 and 19.21h 2107. Instance of sylg 1740. (Contributed by NM, 9-Jan-1993.) (Revised by BJ, 31-Mar-2021.) |
Ref | Expression |
---|---|
alrimih.1 | ⊢ (𝜑 → ∀𝑥𝜑) |
alrimih.2 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimih | ⊢ (𝜑 → ∀𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimih.1 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alrimih.2 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | sylg 1740 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1713 ax-4 1728 |
This theorem is referenced by: nexdh 1779 albidh 1780 exbidhOLD 1782 alrimiv 1842 ax12i 1866 cbvaliw 1920 nf5dh 2013 alrimi 2069 hbnd 2132 cbv3hvOLD 2161 alrimiOLD 2180 aevALTOLD 2309 eujustALT 2461 axi5r 2582 hbralrimi 2937 bnj1093 30302 bj-ax12iOLD 31804 bj-abv 32093 bj-ab0 32094 mpt2bi123f 33141 axc4i-o 33201 equidq 33227 aev-o 33234 ax12f 33243 axc5c4c711 37624 hbimpg 37791 gen11nv 37863 |
Copyright terms: Public domain | W3C validator |