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

Theorem sbcbii 2845
 Description: Formula-building inference rule 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 2844 . 2 (⊤ → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
43trud 1268 1 ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)
 Colors of variables: wff set class Syntax hints:   ↔ wb 102  ⊤wtru 1260  [wsbc 2787 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-sbc 2788 This theorem is referenced by:  eqsbc3r  2846  sbc3an  2847  sbccomlem  2860  sbccom  2861  sbcabel  2867  csbco  2889  sbcnel12g  2895  sbcne12g  2896  sbccsbg  2906  sbccsb2g  2907  csbnestgf  2926  csbabg  2935  sbcssg  3358  sbcrel  4454  difopab  4497  sbcfung  4953  f1od2  5884  mpt2xopovel  5887
 Copyright terms: Public domain W3C validator