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

Theorem bibi1d 310
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 309 . 2  |-  ( ph  ->  ( ( th  <->  ps )  <->  ( th  <->  ch ) ) )
3 bicom 191 . 2  |-  ( ( ps  <->  th )  <->  ( th  <->  ps ) )
4 bicom 191 . 2  |-  ( ( ch  <->  th )  <->  ( th  <->  ch ) )
52, 3, 43bitr4g 279 1  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  bibi12d  312  bibi1  317  biass  348  eubid  2163  axext3  2279  bm1.1  2281  eqeq1  2302  pm13.183  2921  elabgt  2924  mob  2960  sbctt  3066  sbcabel  3081  isoeq2  5833  caovcang  6037  domunfican  7145  axacndlem4  8248  axacnd  8250  expeq0  11148  prmdvdsexp  12809  isacs  13569  acsfn  13577  tsrlemax  14345  odeq  14881  isslw  14935  isabv  15600  t0sep  17068  xkopt  17365  kqt0lem  17443  r0sep  17455  nrmr0reg  17456  ismet  17904  isxmet  17905  stdbdxmet  18077  xrsxmet  18331  iccpnfcnv  18458  mdegle0  19479  isppw2  20369  hvaddcan  21665  eigre  22431  xrge0iifcnv  23330  eupath2lem1  23916  relexpind  24052  dfrtrclrec2  24055  isoriso  25315  oriso  25317  grpodrcan  25478  grpodlcan  25479  fil2ss  25660  isded  25839  dedi  25840  subtr2  26328  nn0prpwlem  26341  nn0prpw  26342  zindbi  27134  expdioph  27219  islssfg2  27272  pm14.122b  27726  bnj1468  29194
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