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

Step	Hyp	Ref	Expression
1		imbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	bibi2d 318	. 2 |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )
3		bicom 200	. 2 |- ( ( ps <-> th ) <-> ( th <-> ps ) )
4		bicom 200	. 2 |- ( ( ch <-> th ) <-> ( th <-> ch ) )
5	2, 3, 4	3bitr4g 288	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )

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  2274  axext3  2425  bm1.1  2427  bm1.1OLD  2428  eqeq1  2449  pm13.183  3105  elabgt  3108  elrab3t  3121  mob  3146  sbctt  3262  sbcabel  3280  isoeq2  6016  caovcang  6269  domunfican  7589  axacndlem4  8782  axacnd  8784  expeq0  11899  prmdvdsexp  13805  isacs  14594  acsfn  14602  tsrlemax  15395  odeq  16058  isslw  16112  isabv  16909  t0sep  18933  xkopt  19233  kqt0lem  19314  r0sep  19326  nrmr0reg  19327  ismet  19903  isxmet  19904  stdbdxmet  20095  xrsxmet  20391  iccpnfcnv  20521  mdegle0  21553  isppw2  22458  cusgrauvtxb  23409  eupath2lem1  23603  hvaddcan  24477  eigre  25244  xrge0iifcnv  26368  sgn0bi  26935  signswch  26967  relexpind  27347  dfrtrclrec2  27350  ftc1anclem6  28477  subtr2  28515  nn0prpwlem  28522  nn0prpw  28523  zindbi  29292  expdioph  29377  islssfg2  29429  pm14.122b  29682  eleclclwwlkn  30512  bnj1468  31844  bj-axext3  32294