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  3170  eloprabga  6165  ereldm  6842  mapen  7136  ordiso2  7365  subcan  8571  conjmulap  9049  ltrec  9203  divelunit  10383  fseq1m1p1  10480  fzm1  10485  qsqeqor  11065  fihashneq0  11211  hashfacen  11262  hashf1  11265  ccat0  11342  cvg1nlemcau  11728  lenegsq  11839  dvdsmod  12607  bitsmod  12701  bezoutlemle  12763  rpexp  12909  qnumdenbi  12948  eulerthlemh  12987  odzdvds  13002  pcelnn  13078  ballotfilemfc0  13210  ballotfilemfcc  13211  grpidpropdg  13671  sgrppropd  13705  mndpropd  13730  mhmpropd  13750  grppropd  13799  ghmnsgima  14048  cmnpropd  14075  qusecsub  14112  rngpropd  14229  ringpropd  14316  dvdsrpropdg  14427  resrhm2b  14530  opprdrng  14593  lmodprop2d  14657  lsspropdg  14740  zndvds0  14957  bdxmet  15525  txmetcnp  15542  cnmet  15554  lgsne0  16071  lgsabs1  16072  gausslemma2dlem1a  16091  lgsquadlem2  16111  usgredg2v  16379  wlkeq  16509  eupth2lem3lem3fi  16625  eupth2lem3lem6fi  16626