Theorem 3bitr4rd 286

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

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

Assertion

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

Proof of Theorem 3bitr4rd

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

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

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 185

This theorem is referenced by:  inimasn  5249  oacan  6979  ecdmn0  7135  wemapwe  7920  wemapweOLD  7921  r1pw  8044  adderpqlem  9115  mulerpqlem  9116  lterpq  9131  ltanq  9132  genpass  9170  readdcan  9535  lemuldiv  10203  msq11  10225  avglt2  10555  qbtwnre  11161  iooshf  11366  clim2c  12975  lo1o1  13002  climabs0  13055  reef11  13395  absefib  13474  efieq1re  13475  pc2dvds  13937  pcmpt  13946  subsubc  14755  odmulgid  16046  gexdvds  16074  submcmn2  16314  obslbs  18135  cnntr  18859  cndis  18875  cnindis  18876  cnpdis  18877  lmres  18884  cmpfi  18991  ist0-4  19282  txhmeo  19356  tsmssubm  19696  blin  19976  cncfmet  20464  icopnfcnv  20494  lmmbrf  20753  iscauf  20771  causs  20789  mbfposr  21110  itg2gt0  21218  limcflf  21336  limcres  21341  lhop1  21466  dvdsr1p  21613  fsumvma2  22533  vmasum  22535  chpchtsum  22538  bposlem1  22603  iscgrgd  22946  lnrot1  23010  eqeelen  23118  nbgraeledg  23309  nb3graprlem2  23328  cusgra3v  23340  cusgrauvtxb  23372  dmdmd  25672  funcnvmptOLD  25954  funcnvmpt  25955  xrdifh  26038  eulerpartlemgh  26730  signslema  26932  leceifl  28391  iblabsnclem  28426  ftc1anclem6  28443  areacirclem5  28459  areacirc  28460  ellz1  29076  islssfg  29394  proot1ex  29540  el2spthonot0  30361  clwlkisclwwlk2  30423  rusgranumwlks  30545  lsatfixedN  32547  cdlemg10c  34176  diaglbN  34593  dih1  34824  dihglbcpreN  34838  mapdcv  35198