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

Theorem r19.26 2583
 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 108 . . . 4
21ralimi 2520 . . 3
3 simpr 109 . . . 4
43ralimi 2520 . . 3
52, 4jca 304 . 2
6 pm3.2 138 . . . 4
76ral2imi 2522 . . 3
87imp 123 . 2
95, 8impbii 125 1
 Colors of variables: wff set class Syntax hints:   wa 103   wb 104  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:  r19.27v  2584  r19.28v  2585  r19.26-2  2586  r19.26-3  2587  ralbiim  2591  r19.27av  2592  reu8  2908  ssrab  3206  r19.28m  3483  r19.27m  3489  2ralunsn  3761  iuneq2  3865  cnvpom  5125  funco  5207  fncnv  5233  funimaexglem  5250  fnres  5283  fnopabg  5290  mpteqb  5555  eqfnfv3  5564  caoftrn  6051  iinerm  6545  ixpeq2  6650  ixpin  6661  rexanuz  10870  recvguniq  10877  cau3lem  10996  rexanre  11102  bezoutlemmo  11870  sqrt2irr  12016  tgval2  12411  metequiv  12855  metequiv2  12856  mulcncflem  12950  bj-indind  13467
 Copyright terms: Public domain W3C validator