Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reximdv2 | Structured version Visualization version Unicode version |
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.) |
Ref | Expression |
---|---|
reximdv2.1 |
Ref | Expression |
---|---|
reximdv2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximdv2.1 | . . 3 | |
2 | 1 | eximdv 1846 | . 2 |
3 | df-rex 2918 | . 2 | |
4 | df-rex 2918 | . 2 | |
5 | 2, 3, 4 | 3imtr4g 285 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wex 1704 wcel 1990 wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-ex 1705 df-rex 2918 |
This theorem is referenced by: ssrexv 3667 ssimaex 6263 nnsuc 7082 oaass 7641 omeulem1 7662 ssnnfi 8179 findcard3 8203 unfilem1 8224 epfrs 8607 alephval3 8933 isfin7-2 9218 fin1a2lem6 9227 fpwwe2lem12 9463 fpwwe2lem13 9464 inawinalem 9511 ico0 12221 ioc0 12222 r19.2uz 14091 climrlim2 14278 iserodd 15540 ramub2 15718 prmgaplem6 15760 pgpssslw 18029 efgrelexlemb 18163 ablfaclem3 18486 unitgrp 18667 lspsneq 19122 lbsextlem4 19161 neissex 20931 iscnp4 21067 nlly2i 21279 llynlly 21280 restnlly 21285 llyrest 21288 nllyrest 21289 llyidm 21291 nllyidm 21292 qtophmeo 21620 cnpflfi 21803 cnextcn 21871 ivthlem3 23222 ovolicc2lem5 23289 dvfsumrlim 23794 itgsubst 23812 lgsquadlem2 25106 footex 25613 opphllem1 25639 oppperpex 25645 outpasch 25647 ushgredgedg 26121 ushgredgedgloop 26123 cusgrfilem2 26352 cmppcmp 29925 eulerpartlemgvv 30438 eulerpartlemgh 30440 erdszelem7 31179 rellysconn 31233 trpredrec 31738 ivthALT 32330 fnessref 32352 phpreu 33393 poimirlem26 33435 itg2gt0cn 33465 frinfm 33530 sstotbnd2 33573 heiborlem3 33612 isdrngo3 33758 dihjat1lem 36717 dvh1dim 36731 dochsatshp 36740 lcfl6 36789 mapdval2N 36919 mapdpglem2 36962 hdmaprnlem10N 37151 pellexlem5 37397 pell14qrss1234 37420 pell1qrss14 37432 pellfundglb 37449 lnr2i 37686 hbtlem6 37699 |
Copyright terms: Public domain | W3C validator |