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

Theorem sbcbii 2996
Description: Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005.)
Hypothesis
Ref Expression
sbcbii.1 (𝜑𝜓)
Assertion
Ref Expression
sbcbii ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)

Proof of Theorem sbcbii
StepHypRef Expression
1 sbcbii.1 . . . 4 (𝜑𝜓)
21a1i 9 . . 3 (⊤ → (𝜑𝜓))
32sbcbidv 2995 . 2 (⊤ → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
43mptru 1344 1 ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wtru 1336  [wsbc 2937
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-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-sbc 2938
This theorem is referenced by:  eqsbc3r  2997  sbc3an  2998  sbccomlem  3011  sbccom  3012  sbcabel  3018  csbco  3041  csbcow  3042  sbcnel12g  3048  sbcne12g  3049  sbccsbg  3060  sbccsb2g  3061  csbnestgf  3083  csbabg  3092  sbcssg  3503  sbcrel  4672  difopab  4719  sbcfung  5194  f1od2  6182  mpoxopovel  6188  bezoutlemnewy  11879  bezoutlemstep  11880  bezoutlemmain  11881
  Copyright terms: Public domain W3C validator