![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > alrimdv | Structured version Visualization version GIF version |
Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2201 and 19.21v 1943. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
alrimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
alrimdv | ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1914 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | ax-5 1914 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) | |
3 | alrimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 1, 2, 3 | alrimdh 1867 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem is referenced by: sbequ1 2241 ax13lem2 2376 reusv1 5391 zfpair 5415 fliftfun 7296 isofrlem 7324 funcnvuni 7909 f1oweALT 7946 findcard 9151 findcard2 9152 findcard2OLD 9272 dfac5lem4 10108 dfac5 10110 zorn2lem4 10481 genpcl 10990 psslinpr 11013 ltaddpr 11016 ltexprlem3 11020 suplem1pr 11034 uzwo 12882 seqf1o 13996 ramcl 16949 alexsubALTlem3 23522 bj-dvelimdv1 35636 intabssd 42141 frege81 42566 frege95 42580 frege123 42608 frege130 42615 truniALT 43173 ggen31 43177 onfrALTlem2 43178 gen21 43251 gen22 43254 ggen22 43255 |
Copyright terms: Public domain | W3C validator |