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 2062 and 19.21v 1855. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
alrimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
alrimdv | ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1827 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | ax-5 1827 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) | |
3 | alrimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 1, 2, 3 | alrimdh 1777 | 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 ax-5 1827 |
This theorem is referenced by: ax13lem2 2284 reusv1 4792 zfpair 4831 fliftfun 6462 isofrlem 6490 funcnvuni 7012 f1oweALT 7043 findcard 8084 findcard2 8085 dfac5lem4 8832 dfac5 8834 zorn2lem4 9204 genpcl 9709 psslinpr 9732 ltaddpr 9735 ltexprlem3 9739 suplem1pr 9753 uzwo 11627 seqf1o 12704 ramcl 15571 alexsubALTlem3 21663 bj-dvelimdv1 32028 intabssd 36935 frege81 37258 frege95 37272 frege123 37300 frege130 37307 truniALT 37772 ggen31 37781 onfrALTlem2 37782 gen21 37865 gen22 37868 ggen22 37869 |
Copyright terms: Public domain | W3C validator |