![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > ralimia | Structured version Unicode version |
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.) |
Ref | Expression |
---|---|
ralimia.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ralimia |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimia.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a2i 13 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ralimi2 2816 |
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 1592 ax-4 1603 |
This theorem depends on definitions: df-bi 185 df-ral 2804 |
This theorem is referenced by: ralimiaa 2818 ralimi 2819 r19.12 2936 rr19.3v 3208 rr19.28v 3209 exfo 5971 ffvresb 5984 f1mpt 6084 weniso 6155 ixpf 7396 ixpiunwdom 7918 tz9.12lem3 8108 dfac2a 8411 kmlem12 8442 axdc2lem 8729 ac6num 8760 ac6c4 8762 brdom6disj 8811 konigthlem 8844 arch 10688 cshw1 12575 serf0 13277 symgextfo 16047 baspartn 18692 ptcnplem 19327 rngmgmbs4 24057 spanuni 25100 lnopunilem1 25567 finixpnum 28563 indexa 28776 heiborlem5 28863 mzpincl 29219 dfac11 29564 |
Copyright terms: Public domain | W3C validator |