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

Theorem 2alimi 1634
Description: Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
Hypothesis
Ref Expression
alimi.1
Assertion
Ref Expression
2alimi

Proof of Theorem 2alimi
StepHypRef Expression
1 alimi.1 . . 3
21alimi 1633 . 2
32alimi 1633 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393
This theorem is referenced by:  mo3OLD  2324  2mo  2373  2moOLD  2374  2eu6  2383  2eu6OLD  2384  euind  3286  reuind  3303  sbnfc2  3854  opelopabt  4764  ssrel  5096  ssrelrel  5108  opabbrex  6339  fnoprabg  6403  tz7.48lem  7125  ssrelf  27466  mpt2bi123f  30571  mptbi12f  30575  ismrc  30633  19.33-2  31287  pm11.63  31301  pm11.71  31303  axc5c4c711to11  31312  bj-3exbi  34207
This theorem was proved from axioms:  ax-mp 5  ax-gen 1618  ax-4 1631
  Copyright terms: Public domain W3C validator