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

Theorem bibi1d 222
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 221 . 2  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
3 bicom 128 . 2  |-  ( ( ps  <->  th )  <->  ( th  <->  ps ) )
4 bicom 128 . 2  |-  ( ( ch  <->  th )  <->  ( th  <->  ch ) )
52, 3, 43bitr4g 212 1  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bibi12d  224  bibi1  229  biassdc  1286  eubidh  1906  eubid  1907  axext3  2023  bm1.1  2025  eqeq1  2046  pm13.183  2681  elabgt  2684  elrab3t  2697  mob  2723  sbctt  2824  sbcabel  2839  isoeq2  5442  caovcang  5662  expap0  9285  bdsepnft  10007  bdsepnfALT  10009  strcollnft  10109  strcollnfALT  10111
  Copyright terms: Public domain W3C validator