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

Theorem bibi2d 230
Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
Hypothesis
Ref Expression
imbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
bibi2d  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )

Proof of Theorem bibi2d
StepHypRef Expression
1 imbid.1 . . . . 5  |-  ( ph  ->  ( ps  <->  ch )
)
21pm5.74i 178 . . . 4  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
32bibi2i 225 . . 3  |-  ( ( ( ph  ->  th )  <->  (
ph  ->  ps ) )  <-> 
( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
4 pm5.74 177 . . 3  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ps ) ) )
5 pm5.74 177 . . 3  |-  ( (
ph  ->  ( th  <->  ch )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
63, 4, 53bitr4i 210 . 2  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ph  ->  ( th  <->  ch ) ) )
76pm5.74ri 179 1  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
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:  bibi1d  231  bibi12d  233  biantr  894  bimsc1  905  eujust  1945  euf  1948  ceqex  2730  reu6i  2792  axsep2  3917  zfauscl  3918  copsexg  4027  euotd  4037  cnveq0  4827  iotaval  4928  iota5  4937  eufnfv  5442  isoeq1  5493  isoeq3  5495  isores2  5505  isores3  5507  isotr  5508  isoini2  5510  riota5f  5544  caovordg  5720  caovord  5724  dfoprab4f  5871  frecabcl  6069  nnaword  6172  xpf1o  6407  ltanqg  6722  ltmnqg  6723  ltasrg  7079  axpre-ltadd  7184  prmdvdsexp  10752  bdsep2  10962  bdzfauscl  10966  strcoll2  11063  sscoll2  11068
  Copyright terms: Public domain W3C validator