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  2158  eujustALT  2159  euf  2162  ceqex  2911  reu6i  2969  sbc2or  3012  axrep1  4148  axrep2  4149  axrep3  4150  zfrepclf  4153  axsep2  4158  zfauscl  4159  copsexg  4268  euotd  4283  cnveq0  5146  iotaval  5246  iota5  5255  eufnfv  5768  isoeq1  5832  isoeq3  5834  isores2  5846  isores3  5848  isotr  5849  isoini2  5852  caovordg  6043  caovord  6047  dfoprab4f  6194  riota5f  6345  seqomlem2  6479  xpf1o  7039  aceq0  7761  dfac5  7771  zfac  8102  zfcndrep  8252  zfcndac  8257  ltasr  8738  axpre-ltadd  8805  absmod0  11804  absz  11812  smuval2  12689  prmdvdsexp  12809  isacs2  13571  isacs1i  13575  mreacs  13576  abvfval  15599  abvpropd  15623  isclo2  16841  t0sep  17068  kqt0lem  17443  r0sep  17455  iccpnfcnv  18458  rolle  19353  ismndo2  21028  eigre  22431  xrge0iifcnv  23330  cvmlift2lem13  23861  isoriso  25315  isoriso2  25316  isded  25839  dedi  25840  sgplpte21a  26236  nn0prpwlem  26341  nn0prpw  26342  mrefg2  26885  zindbi  27134  jm2.19lem3  27187  iotavalb  27733  fargshiftfo  28383  islaut  30894  ispautN  30910
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