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

Theorem sbcbii 2938
 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 2937 . 2 (⊤ → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
43mptru 1323 1 ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)
 Colors of variables: wff set class Syntax hints:   ↔ wb 104  ⊤wtru 1315  [wsbc 2880 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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-sbc 2881 This theorem is referenced by:  eqsbc3r  2939  sbc3an  2940  sbccomlem  2953  sbccom  2954  sbcabel  2960  csbco  2982  sbcnel12g  2988  sbcne12g  2989  sbccsbg  2999  sbccsb2g  3000  csbnestgf  3020  csbabg  3029  sbcssg  3440  sbcrel  4593  difopab  4640  sbcfung  5115  f1od2  6098  mpoxopovel  6104  bezoutlemnewy  11591  bezoutlemstep  11592  bezoutlemmain  11593
 Copyright terms: Public domain W3C validator