Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralimia | Structured version Visualization 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 14 | . 2 |
3 | 2 | ralimi2 2949 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wcel 1990 wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-ral 2917 |
This theorem is referenced by: ralimiaa 2951 ralimi 2952 r19.12 3063 rr19.3v 3345 rr19.28v 3346 exfo 6377 ffvresb 6394 f1mpt 6518 weniso 6604 ixpf 7930 ixpiunwdom 8496 tz9.12lem3 8652 dfac2a 8952 kmlem12 8983 axdc2lem 9270 ac6num 9301 ac6c4 9303 brdom6disj 9354 konigthlem 9390 arch 11289 cshw1 13568 serf0 14411 symgextfo 17842 baspartn 20758 ptcnplem 21424 spanuni 28403 lnopunilem1 28869 phpreu 33393 finixpnum 33394 poimirlem26 33435 indexa 33528 heiborlem5 33614 rngmgmbs4 33730 mzpincl 37297 dfac11 37632 stgoldbwt 41664 2zrngnmlid2 41951 |
Copyright terms: Public domain | W3C validator |