MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralimia Unicode version

Theorem ralimia 2848
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
Hypothesis
Ref Expression
ralimia.1
Assertion
Ref Expression
ralimia

Proof of Theorem ralimia
StepHypRef Expression
1 ralimia.1 . . 3
21a2i 13 . 2
32ralimi2 2847 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  A.wral 2807
This theorem is referenced by:  ralimiaa  2849  ralimi  2850  r19.12  2983  rr19.3v  3241  rr19.28v  3242  exfo  6049  ffvresb  6062  f1mpt  6169  weniso  6250  ixpf  7511  ixpiunwdom  8038  tz9.12lem3  8228  dfac2a  8531  kmlem12  8562  axdc2lem  8849  ac6num  8880  ac6c4  8882  brdom6disj  8931  konigthlem  8964  arch  10817  cshw1  12790  serf0  13503  symgextfo  16447  baspartn  19455  ptcnplem  20122  rngmgmbs4  25419  spanuni  26462  lnopunilem1  26929  finixpnum  30038  indexa  30224  heiborlem5  30311  mzpincl  30666  dfac11  31008  2zrngnmlid2  32757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ral 2812
  Copyright terms: Public domain W3C validator