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

Theorem ralimia 2551
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 2550 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2160  wral 2468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460
This theorem depends on definitions:  df-bi 117  df-ral 2473
This theorem is referenced by:  ralimiaa  2552  ralimi  2553  r19.12  2596  rr19.3v  2891  rr19.28v  2892  ffvresb  5700  f1mpt  5793  ixpf  6746  exmidontri2or  7272  peano2nnnn  7882  peano5nnnn  7921  peano5nni  8952  peano2nn  8961  serf0  11392  baspartn  14007  tridceq  15263
  Copyright terms: Public domain W3C validator