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

Theorem bibi2d 310
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 237 . . . 4  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
32bibi2i 305 . . 3  |-  ( ( ( ph  ->  th )  <->  (
ph  ->  ps ) )  <-> 
( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
4 pm5.74 236 . . 3  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ps ) ) )
5 pm5.74 236 . . 3  |-  ( (
ph  ->  ( th  <->  ch )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
63, 4, 53bitr4i 269 . 2  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ph  ->  ( th  <->  ch ) ) )
76pm5.74ri 238 1  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  bibi1d  311  bibi12d  313  biantr  898  bimsc1  905  eujust  2283  eujustALT  2284  euf  2287  ceqex  3066  reu6i  3125  sbc2or  3169  axrep1  4321  axrep2  4322  axrep3  4323  zfrepclf  4326  axsep2  4331  zfauscl  4332  copsexg  4442  euotd  4457  cnveq0  5327  iotaval  5429  iota5  5438  eufnfv  5972  isoeq1  6039  isoeq3  6041  isores2  6053  isores3  6055  isotr  6056  isoini2  6059  caovordg  6254  caovord  6258  dfoprab4f  6405  riota5f  6574  seqomlem2  6708  xpf1o  7269  aceq0  7999  dfac5  8009  zfac  8340  zfcndrep  8489  zfcndac  8494  ltasr  8975  axpre-ltadd  9042  absmod0  12108  absz  12116  smuval2  12994  prmdvdsexp  13114  isacs2  13878  isacs1i  13882  mreacs  13883  abvfval  15906  abvpropd  15930  isclo2  17152  t0sep  17388  kqt0lem  17768  r0sep  17780  iccpnfcnv  18969  rolle  19874  fargshiftfo  21625  ismndo2  21933  eigre  23338  xrge0iifcnv  24319  cvmlift2lem13  25002  iota5f  25182  nn0prpwlem  26325  nn0prpw  26326  mrefg2  26761  zindbi  27009  jm2.19lem3  27062  iotavalb  27607  2wlkeq  28303  islaut  30880  ispautN  30896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator