New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ralimi GIF version

Theorem ralimi 2689
 Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralimi.1 (φψ)
Assertion
Ref Expression
ralimi (x A φx A ψ)

Proof of Theorem ralimi
StepHypRef Expression
1 ralimi.1 . . 3 (φψ)
21a1i 10 . 2 (x A → (φψ))
32ralimia 2687 1 (x A φx A ψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1710  ∀wral 2614 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557 This theorem depends on definitions:  df-bi 177  df-ral 2619 This theorem is referenced by:  ral2imi  2690  r19.26  2746  r19.29  2754  rr19.3v  2980  rr19.28v  2981  reu3  3026  uniiunlem  3353  reupick2  3541  uniss2  3922  ss2iun  3984  iineq2  3986  iunss2  4011  fununi  5160  fun11uni  5162  dff3  5420  dffo5  5424  ffvresb  5431  dmmptg  5684  fnmpt  5689  fnmpt2  5732
 Copyright terms: Public domain W3C validator