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

Theorem ralimia 2518
 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 2517 1
 Colors of variables: wff set class Syntax hints:   wi 4   wcel 2128  wral 2435 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 1427  ax-gen 1429 This theorem depends on definitions:  df-bi 116  df-ral 2440 This theorem is referenced by:  ralimiaa  2519  ralimi  2520  r19.12  2563  rr19.3v  2851  rr19.28v  2852  ffvresb  5627  f1mpt  5716  ixpf  6658  exmidontri2or  7161  peano2nnnn  7756  peano5nnnn  7795  peano5nni  8819  peano2nn  8828  serf0  11231  baspartn  12408  tridceq  13590
 Copyright terms: Public domain W3C validator