Theorem 3bitr4d 218

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 189	. 2 |- ( ph -> ( ps <-> ta ) )
5	1, 4	bitrd 186	1 |- ( ph -> ( th <-> ta ) )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  dfbi3dc  1333  xordidc  1335  19.32dc  1614  r19.32vdc  2516  opbrop  4517  fvopab3g  5377  respreima  5427  fmptco  5464  cocan1  5566  cocan2  5567  brtposg  6019  nnmword  6275  swoer  6318  erth  6334  brecop  6380  ecopovsymg  6389  xpdom2  6545  pitric  6878  ltexpi  6894  ltapig  6895  ltmpig  6896  ltanqg  6957  ltmnqg  6958  enq0breq  6993  genpassl  7081  genpassu  7082  1idprl  7147  1idpru  7148  caucvgprlemcanl  7201  ltasrg  7314  prsrlt  7330  caucvgsrlemoffcau  7341  axpre-ltadd  7419  subsub23  7685  leadd1  7906  lemul1  8068  reapmul1lem  8069  reapmul1  8070  reapadd1  8071  apsym  8081  apadd1  8083  apti  8097  lediv1  8328  lt2mul2div  8338  lerec  8343  ltdiv2  8346  lediv2  8350  le2msq  8360  avgle1  8654  avgle2  8655  nn01to3  9100  qapne  9122  cnref1o  9131  xleneg  9297  iooneg  9403  iccneg  9404  iccshftr  9409  iccshftl  9411  iccdil  9413  icccntr  9415  fzsplit2  9462  fzaddel  9470  fzrev  9494  elfzo  9556  fzon  9573  elfzom1b  9636  ioo0  9667  ico0  9669  ioc0  9670  flqlt  9686  negqmod0  9734  frec2uzled  9832  expeq0  9982  nn0opthlem1d  10124  leisorel  10238  cjreb  10296  abs00  10493  ltmininf  10661  tanaddaplem  11025  nndivdvds  11076  moddvds  11079  modmulconst  11102  oddm1even  11149  ltoddhalfle  11167  dvdssq  11294  phiprmpw  11472