Theorem bibi1d 333

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 332	. 2 |- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )
3		bicom 212	. 2 |- ( ( ps <-> th ) <-> ( th <-> ps ) )
4		bicom 212	. 2 |- ( ( ch <-> th ) <-> ( th <-> ch ) )
5	2, 3, 4	3bitr4g 303	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  bibi12d  335  bibi1  341  biass  374  eubid  2488  axext3  2604  axext3ALT  2605  bm1.1  2607  eqeq1dALT  2625  pm13.183  3344  elabgt  3347  elrab3t  3362  mob  3388  reu6  3395  sbctt  3500  sbcabel  3517  isoeq2  6568  caovcang  6835  domunfican  8233  axacndlem4  9432  axacnd  9434  expeq0  12890  dfrtrclrec2  13797  relexpind  13804  sumodd  15111  prmdvdsexp  15427  isacs  16312  acsfn  16320  tsrlemax  17220  odeq  17969  isslw  18023  isabv  18819  t0sep  21128  xkopt  21458  kqt0lem  21539  r0sep  21551  nrmr0reg  21552  ismet  22128  isxmet  22129  stdbdxmet  22320  xrsxmet  22612  iccpnfcnv  22743  mdegle0  23837  isppw2  24841  eleclclwwlksn  26953  eupth2lem1  27078  hvaddcan  27927  eigre  28694  xrge0iifcnv  29979  sgn0bi  30609  signswch  30638  bnj1468  30916  br1steqgOLD  31674  br2ndeqgOLD  31675  subtr2  32309  nn0prpwlem  32317  nn0prpw  32318  bj-axext3  32769  dfgcd3  33170  ftc1anclem6  33490  zindbi  37511  expdioph  37590  islssfg2  37641  eliunov2  37971  pm14.122b  38624