![]() |
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 2198 and 19.21v 1940. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
alrimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
alrimdv | ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1911 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | ax-5 1911 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) | |
3 | alrimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 1, 2, 3 | alrimdh 1864 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1537 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1795 ax-4 1809 ax-5 1911 |
This theorem is referenced by: sbequ1 2238 ax13lem2 2373 reusv1 5394 zfpair 5418 fliftfun 7311 isofrlem 7339 funcnvuni 7924 f1oweALT 7961 findcard 9165 findcard2 9166 findcard2OLD 9286 dfac5lem4 10123 dfac5 10125 zorn2lem4 10496 genpcl 11005 psslinpr 11028 ltaddpr 11031 ltexprlem3 11035 suplem1pr 11049 uzwo 12899 seqf1o 14013 ramcl 16966 alexsubALTlem3 23773 bj-dvelimdv1 36034 intabssd 42572 frege81 42997 frege95 43011 frege123 43039 frege130 43046 truniALT 43604 ggen31 43608 onfrALTlem2 43609 gen21 43682 gen22 43685 ggen22 43686 |
Copyright terms: Public domain | W3C validator |