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

Theorem bibi1d 312
Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-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 311 . 2  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
3 bicom 193 . 2  |-  ( ( ps  <->  th )  <->  ( th  <->  ps ) )
4 bicom 193 . 2  |-  ( ( ch  <->  th )  <->  ( th  <->  ch ) )
52, 3, 43bitr4g 281 1  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  bibi12d  314  bibi1  319  biass  350  eubid  2290  axext3  2421  bm1.1  2423  eqeq1  2444  pm13.183  3078  elabgt  3081  mob  3118  sbctt  3225  sbcabel  3240  isoeq2  6042  caovcang  6250  domunfican  7381  axacndlem4  8487  axacnd  8489  expeq0  11412  prmdvdsexp  13116  isacs  13878  acsfn  13886  tsrlemax  14654  odeq  15190  isslw  15244  isabv  15909  t0sep  17390  xkopt  17689  kqt0lem  17770  r0sep  17782  nrmr0reg  17783  ismet  18355  isxmet  18356  stdbdxmet  18547  xrsxmet  18842  iccpnfcnv  18971  mdegle0  20002  isppw2  20900  cusgrauvtxb  21507  eupath2lem1  21701  hvaddcan  22574  eigre  23340  xrge0iifcnv  24321  relexpind  25142  dfrtrclrec2  25145  ftc1anclem6  26287  subtr2  26320  nn0prpwlem  26327  nn0prpw  26328  zindbi  27011  expdioph  27096  islssfg2  27148  pm14.122b  27602  bnj1468  29279
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 179
  Copyright terms: Public domain W3C validator