MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbcbii Structured version   Visualization version   GIF version

Theorem sbcbii 3458
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 11 . . 3 (⊤ → (𝜑𝜓))
32sbcbidv 3457 . 2 (⊤ → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
43trud 1484 1 ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wtru 1476  [wsbc 3402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-sbc 3403
This theorem is referenced by:  eqsbc3r  3459  eqsbc3rOLD  3460  sbc3an  3461  sbccomlem  3475  sbccom  3476  sbcrext  3478  sbcrextOLD  3479  sbcabel  3483  csbco  3509  sbcnel12g  3937  sbcne12  3938  csbcom  3946  csbnestgf  3948  sbccsb  3956  sbccsb2  3957  csbab  3960  sbcssg  4035  sbcrel  5128  difopab  5175  sbcfung  5827  tfinds2  6955  mpt2xopovel  7233  f1od2  28887  bnj62  30040  bnj89  30041  bnj156  30050  bnj524  30060  bnj538OLD  30064  bnj610  30071  bnj919  30091  bnj976  30102  bnj110  30182  bnj91  30185  bnj92  30186  bnj106  30192  bnj121  30194  bnj124  30195  bnj125  30196  bnj126  30197  bnj130  30198  bnj154  30202  bnj155  30203  bnj153  30204  bnj207  30205  bnj523  30211  bnj526  30212  bnj539  30215  bnj540  30216  bnj581  30232  bnj591  30235  bnj609  30241  bnj611  30242  bnj934  30259  bnj1000  30265  bnj984  30276  bnj985  30277  bnj1040  30294  bnj1123  30308  bnj1452  30374  bnj1463  30377  sbcalf  33087  sbcexf  33088  sbccom2lem  33099  sbccom2  33100  sbccom2f  33101  sbccom2fi  33102  csbcom2fi  33104  2sbcrex  36366  2sbcrexOLD  36368  sbcrot3  36373  sbcrot5  36374  2rexfrabdioph  36378  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  rmydioph  36599  expdiophlem2  36607  sbcheg  37093  sbc3or  37759  sbcbiiOLD  37762  trsbc  37771  onfrALTlem5  37778  csbabgOLD  38072
  Copyright terms: Public domain W3C validator