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

Theorem bibi2d 311
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 238 . . . 4  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
32bibi2i 306 . . 3  |-  ( ( ( ph  ->  th )  <->  (
ph  ->  ps ) )  <-> 
( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
4 pm5.74 237 . . 3  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ps ) ) )
5 pm5.74 237 . . 3  |-  ( (
ph  ->  ( th  <->  ch )
)  <->  ( ( ph  ->  th )  <->  ( ph  ->  ch ) ) )
63, 4, 53bitr4i 270 . 2  |-  ( (
ph  ->  ( th  <->  ps )
)  <->  ( ph  ->  ( th  <->  ch ) ) )
76pm5.74ri 239 1  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  bibi1d  312  bibi12d  314  biantr  899  bimsc1  906  eujust  2285  eujustALT  2286  euf  2289  ceqex  3068  reu6i  3127  sbc2or  3171  axrep1  4324  axrep2  4325  axrep3  4326  zfrepclf  4329  axsep2  4334  zfauscl  4335  copsexg  4445  euotd  4460  cnveq0  5330  iotaval  5432  iota5  5441  eufnfv  5975  isoeq1  6042  isoeq3  6044  isores2  6056  isores3  6058  isotr  6059  isoini2  6062  caovordg  6257  caovord  6261  dfoprab4f  6408  riota5f  6577  seqomlem2  6711  xpf1o  7272  aceq0  8004  dfac5  8014  zfac  8345  zfcndrep  8494  zfcndac  8499  ltasr  8980  axpre-ltadd  9047  absmod0  12113  absz  12121  smuval2  12999  prmdvdsexp  13119  isacs2  13883  isacs1i  13887  mreacs  13888  abvfval  15911  abvpropd  15935  isclo2  17157  t0sep  17393  kqt0lem  17773  r0sep  17785  iccpnfcnv  18974  rolle  19879  fargshiftfo  21630  ismndo2  21938  eigre  23343  xrge0iifcnv  24324  cvmlift2lem13  25007  iota5f  25187  nn0prpwlem  26339  nn0prpw  26340  mrefg2  26775  zindbi  27023  jm2.19lem3  27076  iotavalb  27621  2wlkeq  28341  islaut  30954  ispautN  30970
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 179
  Copyright terms: Public domain W3C validator