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  2150  axext3  2266  bm1.1  2268  eqeq1  2289  pm13.183  2908  elabgt  2911  mob  2947  sbctt  3053  sbcabel  3068  isoeq2  5817  caovcang  6021  domunfican  7129  axacndlem4  8232  axacnd  8234  expeq0  11132  prmdvdsexp  12793  isacs  13553  acsfn  13561  tsrlemax  14329  odeq  14865  isslw  14919  isabv  15584  t0sep  17052  xkopt  17349  kqt0lem  17427  r0sep  17439  nrmr0reg  17440  ismet  17888  isxmet  17889  stdbdxmet  18061  xrsxmet  18315  iccpnfcnv  18442  mdegle0  19463  isppw2  20353  hvaddcan  21649  eigre  22415  xrge0iifcnv  23315  eupath2lem1  23901  relexpind  24037  dfrtrclrec2  24040  isoriso  25212  oriso  25214  grpodrcan  25375  grpodlcan  25376  fil2ss  25557  isded  25736  dedi  25737  subtr2  26225  nn0prpwlem  26238  nn0prpw  26239  zindbi  27031  expdioph  27116  islssfg2  27169  pm14.122b  27623  bnj1468  28878
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