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

Theorem bibi2d 309
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 236 . . . 4  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
32bibi2i 304 . . 3  |-  ( ( ( ph  ->  th )  <->  (
ph  ->  ps ) )  <-> 
( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
4 pm5.74 235 . . 3  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ps ) ) )
5 pm5.74 235 . . 3  |-  ( (
ph  ->  ( th  <->  ch )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
63, 4, 53bitr4i 268 . 2  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ph  ->  ( th  <->  ch ) ) )
76pm5.74ri 237 1  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  bibi1d  310  bibi12d  312  biantr  897  bimsc1  904  eujust  2145  eujustALT  2146  euf  2149  ceqex  2898  reu6i  2956  sbc2or  2999  axrep1  4132  axrep2  4133  axrep3  4134  zfrepclf  4137  axsep2  4142  zfauscl  4143  copsexg  4252  euotd  4267  cnveq0  5130  iotaval  5230  iota5  5239  eufnfv  5752  isoeq1  5816  isoeq3  5818  isores2  5830  isores3  5832  isotr  5833  isoini2  5836  caovordg  6027  caovord  6031  dfoprab4f  6178  riota5f  6329  seqomlem2  6463  xpf1o  7023  aceq0  7745  dfac5  7755  zfac  8086  zfcndrep  8236  zfcndac  8241  ltasr  8722  axpre-ltadd  8789  absmod0  11788  absz  11796  smuval2  12673  prmdvdsexp  12793  isacs2  13555  isacs1i  13559  mreacs  13560  abvfval  15583  abvpropd  15607  isclo2  16825  t0sep  17052  kqt0lem  17427  r0sep  17439  iccpnfcnv  18442  rolle  19337  ismndo2  21012  eigre  22415  xrge0iifcnv  23315  cvmlift2lem13  23846  isoriso  25212  isoriso2  25213  isded  25736  dedi  25737  sgplpte21a  26133  nn0prpwlem  26238  nn0prpw  26239  mrefg2  26782  zindbi  27031  jm2.19lem3  27084  iotavalb  27630  islaut  30272  ispautN  30288
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 177
  Copyright terms: Public domain W3C validator