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

Theorem bibi1d 232
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 231 . 2  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
3 bicom 139 . 2  |-  ( ( ps  <->  th )  <->  ( th  <->  ps ) )
4 bicom 139 . 2  |-  ( ( ch  <->  th )  <->  ( th  <->  ch ) )
52, 3, 43bitr4g 222 1  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bibi12d  234  bibi1  239  biassdc  1356  eubidh  1981  eubid  1982  axext3  2098  bm1.1  2100  eqeq1  2122  pm13.183  2794  elabgt  2797  elrab3t  2810  mob  2837  sbctt  2945  sbcabel  2960  isoeq2  5669  caovcang  5898  frecabcl  6262  expap0  10263  bezoutlemeu  11591  dfgcd3  11594  bezout  11595  prmdvdsexp  11722  ismet  12408  isxmet  12409  bdsepnft  12887  bdsepnfALT  12889  strcollnft  12984  strcollnfALT  12986
  Copyright terms: Public domain W3C validator