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

Theorem bibi1d 231
Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
imbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
bibi1d  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  th ) ) )

Proof of Theorem bibi1d
StepHypRef Expression
1 imbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21bibi2d 230 . 2  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
3 bicom 138 . 2  |-  ( ( ps  <->  th )  <->  ( th  <->  ps ) )
4 bicom 138 . 2  |-  ( ( ch  <->  th )  <->  ( th  <->  ch ) )
52, 3, 43bitr4g 221 1  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  bibi12d  233  bibi1  238  biassdc  1327  eubidh  1948  eubid  1949  axext3  2065  bm1.1  2067  eqeq1  2088  pm13.183  2733  elabgt  2736  elrab3t  2749  mob  2775  sbctt  2881  sbcabel  2896  isoeq2  5473  caovcang  5693  frecabcl  6048  expap0  9603  bezoutlemeu  10540  dfgcd3  10543  bezout  10544  prmdvdsexp  10671  bdsepnft  10836  bdsepnfALT  10838  strcollnft  10937  strcollnfALT  10939
  Copyright terms: Public domain W3C validator