Theorem 3bitr4d 209

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)

Hypotheses

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

Assertion

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

Proof of Theorem 3bitr4d

Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
2		3bitr4d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3		3bitr4d.3	. . 3 |- ( ph -> ( ta <-> ch ) )
4	2, 3	bitr4d 180	. 2 |- ( ph -> ( ps <-> ta ) )
5	1, 4	bitrd 177	1 |- ( ph -> ( th <-> ta ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  dfbi3dc  1288  xordidc  1290  19.32dc  1569  r19.32vdc  2459  r19.12sn  3436  opbrop  4419  fvopab3g  5245  respreima  5295  fmptco  5330  cocan1  5427  cocan2  5428  brtposg  5869  nnmword  6091  swoer  6134  erth  6150  brecop  6196  ecopovsymg  6205  xpdom2  6305  pitric  6419  ltexpi  6435  ltapig  6436  ltmpig  6437  ltanqg  6498  ltmnqg  6499  enq0breq  6534  genpassl  6622  genpassu  6623  1idprl  6688  1idpru  6689  caucvgprlemcanl  6742  ltasrg  6855  prsrlt  6871  caucvgsrlemoffcau  6882  axpre-ltadd  6960  subsub23  7216  leadd1  7425  lemul1  7584  reapmul1lem  7585  reapmul1  7586  reapadd1  7587  apsym  7597  apadd1  7599  apti  7613  lediv1  7835  lt2mul2div  7845  lerec  7850  ltdiv2  7853  lediv2  7857  le2msq  7867  avgle1  8165  avgle2  8166  nn01to3  8552  qapne  8574  cnref1o  8582  xleneg  8750  iooneg  8856  iccneg  8857  iccshftr  8862  iccshftl  8864  iccdil  8866  icccntr  8868  fzsplit2  8914  fzaddel  8922  fzrev  8946  elfzo  9006  fzon  9022  elfzom1b  9085  flqlt  9125  negqmod0  9173  expeq0  9286  cjreb  9466  abs00  9662