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  931  bimsc1  938  eujust  2270  eujustALT  2271  euf  2278  reu6i  3276  sbc2or  3322  axrep1  4549  axrep2  4550  axrep3  4551  zfrepclf  4554  axsep2  4559  zfauscl  4560  copsexg  4722  copsexgOLD  4723  euotd  4738  cnveq0  5453  iotaval  5552  iota5  5561  eufnfv  6131  isoeq1  6200  isoeq3  6202  isores2  6214  isores3  6216  isotr  6217  isoini2  6220  riota5f  6267  caovordg  6467  caovord  6471  dfoprab4f  6843  seqomlem2  7118  xpf1o  7681  aceq0  8502  dfac5  8512  zfac  8843  zfcndrep  8995  zfcndac  9000  ltasr  9480  axpre-ltadd  9547  absmod0  13118  absz  13126  smuval2  14114  prmdvdsexp  14237  isacs2  15032  isacs1i  15036  mreacs  15037  abvfval  17446  abvpropd  17470  isclo2  19567  t0sep  19803  kqt0lem  20215  r0sep  20227  iccpnfcnv  21422  rolle  22369  fargshiftfo  24616  2wlkeq  24685  ismndo2  25325  eigre  26732  fgreu  27491  fcnvgreu  27492  xrge0iifcnv  27893  cvmlift2lem13  28738  iota5f  29080  nn0prpwlem  30116  nn0prpw  30117  mrefg2  30615  zindbi  30858  jm2.19lem3  30909  iotavalb  31291  bj-axrep1  34257  bj-axrep2  34258  bj-axrep3  34259  bj-axsep2  34376  islaut  35682  ispautN  35698
  Copyright terms: Public domain W3C validator