Theorem 3bitr3d 218

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)

Hypotheses

Ref	Expression
3bitr3d.1	|- ( ph -> ( ps <-> ch ) )
3bitr3d.2	|- ( ph -> ( ps <-> th ) )
3bitr3d.3	|- ( ph -> ( ch <-> ta ) )

Assertion

Ref	Expression
3bitr3d	|- ( ph -> ( th <-> ta ) )

Proof of Theorem 3bitr3d

Step	Hyp	Ref	Expression
1		3bitr3d.2	. . 3 |- ( ph -> ( ps <-> th ) )
2		3bitr3d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3	1, 2	bitr3d 190	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr3d.3	. 2 |- ( ph -> ( ch <-> ta ) )
5	3, 4	bitrd 188	1 |- ( ph -> ( th <-> ta ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  csbcomg  3107  eloprabga  6013  ereldm  6646  mapen  6916  ordiso2  7110  subcan  8298  conjmulap  8773  ltrec  8927  divelunit  10094  fseq1m1p1  10187  fzm1  10192  qsqeqor  10759  fihashneq0  10903  hashfacen  10945  cvg1nlemcau  11166  lenegsq  11277  dvdsmod  12044  bitsmod  12138  bezoutlemle  12200  rpexp  12346  qnumdenbi  12385  eulerthlemh  12424  odzdvds  12439  pcelnn  12515  grpidpropdg  13076  sgrppropd  13115  mndpropd  13142  mhmpropd  13168  grppropd  13219  ghmnsgima  13474  cmnpropd  13501  qusecsub  13537  rngpropd  13587  ringpropd  13670  dvdsrpropdg  13779  resrhm2b  13881  lmodprop2d  13980  lsspropdg  14063  zndvds0  14282  bdxmet  14821  txmetcnp  14838  cnmet  14850  lgsne0  15363  lgsabs1  15364  gausslemma2dlem1a  15383  lgsquadlem2  15403