MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bibi2d Structured version   Unicode version

Theorem bibi2d 318
Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-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 245 . . . 4  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
32bibi2i 313 . . 3  |-  ( ( ( ph  ->  th )  <->  (
ph  ->  ps ) )  <-> 
( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
4 pm5.74 244 . . 3  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ps ) ) )
5 pm5.74 244 . . 3  |-  ( (
ph  ->  ( th  <->  ch )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
63, 4, 53bitr4i 277 . 2  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ph  ->  ( th  <->  ch ) ) )
76pm5.74ri 246 1  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  bibi1d  319  bibi12d  321  biantr  922  bimsc1  929  eujust  2255  eujustALT  2256  euf  2263  eufOLD  2264  reu6i  3149  sbc2or  3194  axrep1  4403  axrep2  4404  axrep3  4405  zfrepclf  4408  axsep2  4413  zfauscl  4414  copsexg  4575  copsexgOLD  4576  euotd  4591  cnveq0  5293  iotaval  5391  iota5  5400  eufnfv  5950  isoeq1  6009  isoeq3  6011  isores2  6023  isores3  6025  isotr  6026  isoini2  6029  riota5f  6076  caovordg  6269  caovord  6273  dfoprab4f  6631  seqomlem2  6905  xpf1o  7472  aceq0  8287  dfac5  8297  zfac  8628  zfcndrep  8780  zfcndac  8785  ltasr  9266  axpre-ltadd  9333  absmod0  12791  absz  12799  smuval2  13677  prmdvdsexp  13799  isacs2  14590  isacs1i  14594  mreacs  14595  abvfval  16902  abvpropd  16926  isclo2  18691  t0sep  18927  kqt0lem  19308  r0sep  19320  iccpnfcnv  20515  rolle  21461  fargshiftfo  23523  ismndo2  23831  eigre  25238  fgreu  25989  xrge0iifcnv  26362  cvmlift2lem13  27203  iota5f  27380  nn0prpwlem  28515  nn0prpw  28516  mrefg2  29041  zindbi  29285  jm2.19lem3  29338  iotavalb  29682  2wlkeq  30286  bj-axrep1  32307  bj-axrep2  32308  bj-axrep3  32309  bj-axsep2  32426  islaut  33725  ispautN  33741
  Copyright terms: Public domain W3C validator