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

Theorem bibi2d 319
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 248 . . . 4  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
32bibi2i 314 . . 3  |-  ( ( ( ph  ->  th )  <->  (
ph  ->  ps ) )  <-> 
( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
4 pm5.74 247 . . 3  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ps ) ) )
5 pm5.74 247 . . 3  |-  ( (
ph  ->  ( th  <->  ch )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
63, 4, 53bitr4i 280 . 2  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ph  ->  ( th  <->  ch ) ) )
76pm5.74ri 249 1  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  bibi1d  320  bibi12d  322  biantr  939  bimsc1  946  eujust  2271  eujustALT  2272  euf  2277  reu6i  3261  sbc2or  3308  axrep1  4537  axrep2  4538  axrep3  4539  zfrepclf  4542  axsep2  4547  zfauscl  4548  copsexg  4706  euotd  4721  cnveq0  5311  iotaval  5576  iota5  5585  eufnfv  6154  isoeq1  6225  isoeq3  6227  isores2  6239  isores3  6241  isotr  6242  isoini2  6245  riota5f  6291  caovordg  6490  caovord  6494  dfoprab4f  6865  seqomlem2  7179  xpf1o  7743  aceq0  8556  dfac5  8566  zfac  8897  zfcndrep  9046  zfcndac  9051  ltasr  9531  axpre-ltadd  9598  absmod0  13366  absz  13374  smuval2  14455  prmdvdsexp  14666  isacs2  15558  isacs1i  15562  mreacs  15563  abvfval  18045  abvpropd  18069  isclo2  20102  t0sep  20338  kqt0lem  20749  r0sep  20761  iccpnfcnv  21970  rolle  22940  fargshiftfo  25364  2wlkeq  25433  ismndo2  26071  eigre  27486  fgreu  28276  fcnvgreu  28277  xrge0iifcnv  28747  cvmlift2lem13  30046  iota5f  30365  nn0prpwlem  30983  nn0prpw  30984  bj-axrep1  31373  bj-axrep2  31374  bj-axrep3  31375  bj-axsep2  31497  wl-eudf  31865  islaut  33617  ispautN  33633  mrefg2  35518  zindbi  35764  jm2.19lem3  35816  iotavalb  36751
  Copyright terms: Public domain W3C validator