Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bj-stan Unicode version

Theorem bj-stan 12940
 Description: The conjunction of two stable formulas is stable. See bj-stim 12939 for implication, stabnot 818 for negation, and bj-stal 12942 for universal quantification. (Contributed by BJ, 24-Nov-2023.)
Assertion
Ref Expression
bj-stan STAB STAB STAB

Proof of Theorem bj-stan
StepHypRef Expression
1 bj-nnan 12933 . . 3
2 anim12 341 . . 3
31, 2syl5 32 . 2
4 df-stab 816 . . 3 STAB
5 df-stab 816 . . 3 STAB
64, 5anbi12i 455 . 2 STAB STAB
7 df-stab 816 . 2 STAB
83, 6, 73imtr4i 200 1 STAB STAB STAB
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103  STAB wstab 815 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-in1 603  ax-in2 604 This theorem depends on definitions:  df-bi 116  df-stab 816 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator