ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralimia GIF version

Theorem ralimia 2531
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 11 . 2 ((𝑥𝐴𝜑) → (𝑥𝐴𝜓))
32ralimi2 2530 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2141  wral 2448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442
This theorem depends on definitions:  df-bi 116  df-ral 2453
This theorem is referenced by:  ralimiaa  2532  ralimi  2533  r19.12  2576  rr19.3v  2869  rr19.28v  2870  ffvresb  5659  f1mpt  5750  ixpf  6698  exmidontri2or  7220  peano2nnnn  7815  peano5nnnn  7854  peano5nni  8881  peano2nn  8890  serf0  11315  baspartn  12842  tridceq  14088
  Copyright terms: Public domain W3C validator