|   | 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 2206 and 19.21v 1938. (Contributed by NM, 10-Feb-1997.) | 
| Ref | Expression | 
|---|---|
| alrimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) | 
| Ref | Expression | 
|---|---|
| alrimdv | ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ax-5 1909 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
| 2 | ax-5 1909 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) | |
| 3 | alrimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 4 | 1, 2, 3 | alrimdh 1862 | 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 1794 ax-4 1808 ax-5 1909 | 
| This theorem is referenced by: sbequ1 2247 ax13lem2 2380 reusv1 5396 zfpair 5420 axprlem3 5424 fliftfun 7333 isofrlem 7361 funcnvuni 7955 f1oweALT 7998 findcard 9204 findcard2 9205 dfac5lem4 10167 dfac5lem4OLD 10169 dfac5 10170 zorn2lem4 10540 genpcl 11049 psslinpr 11072 ltaddpr 11075 ltexprlem3 11079 suplem1pr 11093 uzwo 12954 seqf1o 14085 ramcl 17068 alexsubALTlem3 24058 bj-dvelimdv1 36854 intabssd 43537 frege81 43962 frege95 43976 frege123 44004 frege130 44011 truniALT 44566 ggen31 44570 onfrALTlem2 44571 gen21 44644 gen22 44647 ggen22 44648 relpfrlem 44979 | 
| Copyright terms: Public domain | W3C validator |