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

Theorem ralimia 2538
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 2537 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2148  wral 2455
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 1447  ax-gen 1449
This theorem depends on definitions:  df-bi 117  df-ral 2460
This theorem is referenced by:  ralimiaa  2539  ralimi  2540  r19.12  2583  rr19.3v  2876  rr19.28v  2877  ffvresb  5679  f1mpt  5771  ixpf  6719  exmidontri2or  7241  peano2nnnn  7851  peano5nnnn  7890  peano5nni  8921  peano2nn  8930  serf0  11359  baspartn  13520  tridceq  14774
  Copyright terms: Public domain W3C validator