![]() |
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 1764 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-rex 2743 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-rex 2743 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3imtr4g 274 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 |
This theorem depends on definitions: df-bi 189 df-ex 1664 df-rex 2743 |
This theorem is referenced by: ssrexv 3494 ssimaex 5930 nnsuc 6709 oaass 7262 omeulem1 7283 ssnnfi 7791 findcard3 7814 unfilem1 7835 epfrs 8215 alephval3 8541 isfin7-2 8826 fin1a2lem6 8835 fpwwe2lem12 9066 fpwwe2lem13 9067 inawinalem 9114 ico0 11682 ioc0 11683 r19.2uz 13414 climrlim2 13611 iserodd 14785 ramub2 14971 prmgaplem6 15026 pgpssslw 17266 efgrelexlemb 17400 ablfaclem3 17720 unitgrp 17895 lspsneq 18345 lbsextlem4 18384 neissex 20143 iscnp4 20279 nlly2i 20491 llynlly 20492 restnlly 20497 llyrest 20500 nllyrest 20501 llyidm 20503 nllyidm 20504 qtophmeo 20832 cnpflfi 21014 cnextcn 21082 ivthlem3 22404 ovolicc2lem5 22475 dvfsumrlim 22983 itgsubst 23001 lgsquadlem2 24283 footex 24763 opphllem1 24789 oppperpex 24795 outpasch 24797 nbgraf1olem5 25173 cusgrafilem2 25208 cmppcmp 28685 eulerpartlemgvv 29209 eulerpartlemgh 29211 erdszelem7 29920 rellyscon 29974 trpredrec 30479 ivthALT 30991 fnessref 31013 phpreu 31929 poimirlem26 31966 itg2gt0cn 31997 frinfm 32062 sstotbnd2 32106 heiborlem3 32145 isdrngo3 32198 dihjat1lem 34996 dvh1dim 35010 dochsatshp 35019 lcfl6 35068 mapdval2N 35198 mapdpglem2 35241 hdmaprnlem10N 35430 pellexlem5 35677 pell14qrss1234 35702 pell1qrss14 35714 pellfundglb 35733 lnr2i 35975 hbtlem6 35988 ushgredgedga 39306 ushgredgedgaloop 39308 cusgrfilem2 39517 |
Copyright terms: Public domain | W3C validator |