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

Theorem ss2abi 3169
 Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)
Hypothesis
Ref Expression
ss2abi.1
Assertion
Ref Expression
ss2abi

Proof of Theorem ss2abi
StepHypRef Expression
1 ss2ab 3165 . 2
2 ss2abi.1 . 2
31, 2mpgbir 1429 1
 Colors of variables: wff set class Syntax hints:   wi 4  cab 2125   wss 3071 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-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-in 3077  df-ss 3084 This theorem is referenced by:  abssi  3172  rabssab  3184  pwsnss  3730  iinuniss  3895  pwpwssunieq  3901  abssexg  4106  imassrn  4892  imadiflem  5202  imainlem  5204  fabexg  5310  f1oabexg  5379  tfrcllemssrecs  6249  mapex  6548  tgval  12232  tgvalex  12233
 Copyright terms: Public domain W3C validator