Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bdbi Unicode version

Theorem bdbi 10868
Description: A biconditional between two bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
Hypotheses
Ref Expression
bdbi.1  |- BOUNDED  ph
bdbi.2  |- BOUNDED  ps
Assertion
Ref Expression
bdbi  |- BOUNDED  ( ph  <->  ps )

Proof of Theorem bdbi
StepHypRef Expression
1 bdbi.1 . . . 4  |- BOUNDED  ph
2 bdbi.2 . . . 4  |- BOUNDED  ps
31, 2ax-bdim 10856 . . 3  |- BOUNDED  ( ph  ->  ps )
42, 1ax-bdim 10856 . . 3  |- BOUNDED  ( ps  ->  ph )
53, 4ax-bdan 10857 . 2  |- BOUNDED  ( ( ph  ->  ps )  /\  ( ps 
->  ph ) )
6 dfbi2 380 . 2  |-  ( (
ph 
<->  ps )  <->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )
75, 6bd0r 10867 1  |- BOUNDED  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103  BOUNDED wbd 10854
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-bd0 10855  ax-bdim 10856  ax-bdan 10857
This theorem depends on definitions:  df-bi 115
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator