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

Theorem bibi1d 319
Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 11-May-1993.)
Hypothesis
Ref Expression
imbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
bibi1d  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  th ) ) )

Proof of Theorem bibi1d
StepHypRef Expression
1 imbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21bibi2d 318 . 2  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
3 bicom 200 . 2  |-  ( ( ps  <->  th )  <->  ( th  <->  ps ) )
4 bicom 200 . 2  |-  ( ( ch  <->  th )  <->  ( th  <->  ch ) )
52, 3, 43bitr4g 288 1  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  bibi12d  321  bibi1  327  biass  359  eubid  2288  axext3  2423  axext3OLD  2424  bm1.1  2426  bm1.1OLD  2427  eqeq1dALT  2446  eqeq1OLD  2448  pm13.183  3226  elabgt  3229  elrab3t  3242  mob  3267  sbctt  3384  sbcabel  3402  isoeq2  6201  caovcang  6461  domunfican  7795  axacndlem4  8991  axacnd  8993  expeq0  12178  prmdvdsexp  14237  isacs  15030  acsfn  15038  tsrlemax  15829  odeq  16553  isslw  16607  isabv  17447  t0sep  19803  xkopt  20134  kqt0lem  20215  r0sep  20227  nrmr0reg  20228  ismet  20804  isxmet  20805  stdbdxmet  20996  xrsxmet  21292  iccpnfcnv  21422  mdegle0  22455  isppw2  23367  cusgrauvtxb  24474  eleclclwwlkn  24811  eupath2lem1  24955  hvaddcan  25965  eigre  26732  xrge0iifcnv  27893  sgn0bi  28464  signswch  28496  relexpind  29041  dfrtrclrec2  29044  ftc1anclem6  30071  subtr2  30109  nn0prpwlem  30116  nn0prpw  30117  zindbi  30858  expdioph  30941  islssfg2  30993  pm14.122b  31284  bnj1468  33772  bj-axext3  34237
  Copyright terms: Public domain W3C validator