![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reximdvai | 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, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) |
Ref | Expression |
---|---|
reximdvai.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
reximdvai |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximdvai.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ralrimiv 2812 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | rexim 2864 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl 17 |
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 1680 ax-4 1693 ax-5 1769 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 df-ral 2754 df-rex 2755 |
This theorem is referenced by: reximdv 2873 reximdva 2874 reuind 3255 wefrc 4850 isomin 6258 isofrlem 6261 onfununi 7091 oaordex 7290 odi 7311 omass 7312 omeulem1 7314 noinfep 8196 rankwflemb 8295 infxpenlem 8475 coflim 8722 coftr 8734 zorn2lem7 8963 suplem1pr 9508 axpre-sup 9624 climbdd 13790 filufint 20990 cvati 28075 atcvat4i 28106 mdsymlem2 28113 mdsymlem3 28114 sumdmdii 28124 iccllyscon 30023 dftrpred3g 30524 incsequz2 32124 lcvat 32642 hlrelat3 33023 cvrval3 33024 cvrval4N 33025 2atlt 33050 cvrat4 33054 atbtwnexOLDN 33058 atbtwnex 33059 athgt 33067 2llnmat 33135 lnjatN 33391 2lnat 33395 cdlemb 33405 lhpexle3lem 33622 cdlemf1 34174 cdlemf2 34175 cdlemf 34176 cdlemk26b-3 34518 dvh4dimlem 35057 upbdrech 37598 limcperiod 37794 cncfshift 37837 cncfperiod 37842 |
Copyright terms: Public domain | W3C validator |