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

Theorem r19.26 2435
Description: Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.26

Proof of Theorem r19.26
StepHypRef Expression
1 simpl 102 . . . 4
21ralimi 2378 . . 3
3 simpr 103 . . . 4
43ralimi 2378 . . 3
52, 4jca 290 . 2
6 pm3.2 126 . . . 4
76ral2imi 2379 . . 3
87imp 115 . 2
95, 8impbii 117 1
Colors of variables: wff set class
Syntax hints:   wa 97   wb 98  wral 2300
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335
This theorem depends on definitions:  df-bi 110  df-ral 2305
This theorem is referenced by:  r19.26-2  2436  r19.26-3  2437  ralbiim  2441  r19.27av  2442  reu8  2731  ssrab  3012  r19.28m  3305  r19.27m  3310  2ralunsn  3560  iuneq2  3664  cnvpom  4803  funco  4883  fncnv  4908  funimaexglem  4925  fnres  4958  fnopabg  4965  mpteqb  5204  eqfnfv3  5210  caoftrn  5678  iinerm  6114
  Copyright terms: Public domain W3C validator