|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > alimdv | Structured version Visualization version GIF version | ||
| Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1809. See alimdh 1816 and alimd 2211 for versions without a distinct variable condition. (Contributed by NM, 3-Apr-1994.) | 
| Ref | Expression | 
|---|---|
| alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) | 
| Ref | Expression | 
|---|---|
| alimdv | ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ax-5 1909 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
| 2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 3 | 1, 2 | alimdh 1816 | 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: 2alimdv 1917 ax12v2 2178 ax13lem1 2378 axc16i 2440 mo4 2565 ralimdv2 3162 mo2icl 3719 sstr2OLD 3990 reuss2 4325 ssuni 4931 disjss2 5112 disjss1 5115 disjiun 5130 disjss3 5141 alxfr 5406 axprlem1 5422 axprlem2 5423 axpr 5426 axprOLD 5430 frss 5648 ssrel 5791 ssrelOLD 5792 ssrel2 5794 ssrelrel 5805 iotavalOLD 6534 fvn0ssdmfun 7093 dff3 7119 dfwe2 7795 trom 7897 findcard3 9319 findcard3OLD 9320 dffi2 9464 indcardi 10082 zorn2lem4 10540 uzindi 14024 caubnd 15398 ramtlecl 17039 psgnunilem4 19516 nrhmzr 20538 dfconn2 23428 wilthlem3 27114 disjss1f 32586 ssrelf 32628 axsepg2 35097 axsepg2ALT 35098 ss2mcls 35574 mclsax 35575 wzel 35826 onsuct0 36443 bj-zfauscl 36926 wl-ax13lem1 37496 axc11next 44430 traxext 44999 iscnrm3lem2 48839 setrec1lem2 49262 | 
| Copyright terms: Public domain | W3C validator |