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  5410  oacan  7196  ecdmn0  7353  wemapwe  8139  wemapweOLD  8140  r1pw  8263  adderpqlem  9332  mulerpqlem  9333  lterpq  9348  ltanq  9349  genpass  9387  readdcan  9754  lemuldiv  10427  msq11  10449  avglt2  10780  qbtwnre  11404  iooshf  11609  clim2c  13304  lo1o1  13331  climabs0  13384  reef11  13728  absefib  13807  efieq1re  13808  pc2dvds  14276  pcmpt  14285  subsubc  15093  odmulgid  16447  gexdvds  16475  submcmn2  16718  obslbs  18631  cnntr  19646  cndis  19662  cnindis  19663  cnpdis  19664  lmres  19671  cmpfi  19778  ist0-4  20100  txhmeo  20174  tsmssubm  20514  blin  20794  cncfmet  21282  icopnfcnv  21312  lmmbrf  21571  iscauf  21589  causs  21607  mbfposr  21929  itg2gt0  22037  limcflf  22155  limcres  22160  lhop1  22285  dvdsr1p  22432  fsumvma2  23358  vmasum  23360  chpchtsum  23363  bposlem1  23428  iscgrgd  23774  lnrot1  23872  eqeelen  24076  nbgraeledg  24299  nb3graprlem2  24321  cusgra3v  24333  cusgrauvtxb  24365  clwlkisclwwlk2  24659  el2spthonot0  24740  rusgranumwlks  24825  dmdmd  27088  funcnvmptOLD  27378  funcnvmpt  27379  xrdifh  27460  ismntop  27874  eulerpartlemgh  28187  signslema  28389  leceifl  30016  iblabsnclem  30050  ftc1anclem6  30067  areacirclem5  30083  areacirc  30084  ellz1  30672  islssfg  30988  proot1ex  31134  eliooshift  31477  clim2cf  31564  lsatfixedN  34457  cdlemg10c  36088  diaglbN  36505  dih1  36736  dihglbcpreN  36750  mapdcv  37110