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

Theorem bibi2d 325
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 253 . . . 4  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
32bibi2i 320 . . 3  |-  ( ( ( ph  ->  th )  <->  (
ph  ->  ps ) )  <-> 
( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
4 pm5.74 252 . . 3  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ps ) ) )
5 pm5.74 252 . . 3  |-  ( (
ph  ->  ( th  <->  ch )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
63, 4, 53bitr4i 285 . 2  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ph  ->  ( th  <->  ch ) ) )
76pm5.74ri 254 1  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  bibi1d  326  bibi12d  328  biantr  945  bimsc1  953  eujust  2321  eujustALT  2322  euf  2327  reu6i  3217  sbc2or  3264  axrep1  4509  axrep2  4510  axrep3  4511  zfrepclf  4514  axsep2  4519  zfauscl  4520  copsexg  4687  euotd  4702  cnveq0  5299  iotaval  5564  iota5  5573  eufnfv  6156  isoeq1  6228  isoeq3  6230  isores2  6242  isores3  6244  isotr  6245  isoini2  6248  riota5f  6294  caovordg  6495  caovord  6499  dfoprab4f  6870  seqomlem2  7186  xpf1o  7752  aceq0  8567  dfac5  8577  zfac  8908  zfcndrep  9057  zfcndac  9062  ltasr  9542  axpre-ltadd  9609  absmod0  13443  absz  13451  smuval2  14535  prmdvdsexp  14746  isacs2  15637  isacs1i  15641  mreacs  15642  abvfval  18124  abvpropd  18148  isclo2  20181  t0sep  20417  kqt0lem  20828  r0sep  20840  iccpnfcnv  22050  rolle  23021  fargshiftfo  25445  2wlkeq  25514  ismndo2  26154  eigre  27569  fgreu  28349  fcnvgreu  28350  xrge0iifcnv  28813  cvmlift2lem13  30110  iota5f  30429  nn0prpwlem  31049  nn0prpw  31050  bj-axrep1  31469  bj-axrep2  31470  bj-axrep3  31471  bj-axsep2  31596  wl-eudf  31971  islaut  33719  ispautN  33735  mrefg2  35620  zindbi  35865  jm2.19lem3  35917  iotavalb  36851
  Copyright terms: Public domain W3C validator