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  929  bimsc1  936  eujust  2277  eujustALT  2278  euf  2285  eufOLD  2286  reu6i  3294  sbc2or  3340  axrep1  4559  axrep2  4560  axrep3  4561  zfrepclf  4564  axsep2  4569  zfauscl  4570  copsexg  4732  copsexgOLD  4733  euotd  4748  cnveq0  5463  iotaval  5562  iota5  5571  eufnfv  6134  isoeq1  6203  isoeq3  6205  isores2  6217  isores3  6219  isotr  6220  isoini2  6223  riota5f  6270  caovordg  6466  caovord  6470  dfoprab4f  6842  seqomlem2  7116  xpf1o  7679  aceq0  8499  dfac5  8509  zfac  8840  zfcndrep  8992  zfcndac  8997  ltasr  9477  axpre-ltadd  9544  absmod0  13099  absz  13107  smuval2  13991  prmdvdsexp  14114  isacs2  14908  isacs1i  14912  mreacs  14913  abvfval  17267  abvpropd  17291  isclo2  19383  t0sep  19619  kqt0lem  20000  r0sep  20012  iccpnfcnv  21207  rolle  22154  fargshiftfo  24342  2wlkeq  24411  ismndo2  25051  eigre  26458  fgreu  27213  xrge0iifcnv  27579  cvmlift2lem13  28428  iota5f  28605  nn0prpwlem  29745  nn0prpw  29746  mrefg2  30271  zindbi  30514  jm2.19lem3  30565  iotavalb  30943  bj-axrep1  33473  bj-axrep2  33474  bj-axrep3  33475  bj-axsep2  33592  islaut  34897  ispautN  34913
  Copyright terms: Public domain W3C validator