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  5346  oacan  7133  ecdmn0  7290  wemapwe  8070  wemapweOLD  8071  r1pw  8194  adderpqlem  9261  mulerpqlem  9262  lterpq  9277  ltanq  9278  genpass  9316  readdcan  9683  lemuldiv  10358  msq11  10380  avglt2  10712  qbtwnre  11337  iooshf  11542  clim2c  13349  lo1o1  13376  climabs0  13429  reef11  13875  absefib  13954  efieq1re  13955  pc2dvds  14423  pcmpt  14432  subsubc  15278  odmulgid  16712  gexdvds  16740  submcmn2  16983  obslbs  18871  cnntr  19881  cndis  19897  cnindis  19898  cnpdis  19899  lmres  19906  cmpfi  20013  ist0-4  20334  txhmeo  20408  tsmssubm  20748  blin  21028  cncfmet  21516  icopnfcnv  21546  lmmbrf  21805  iscauf  21823  causs  21841  mbfposr  22163  itg2gt0  22271  limcflf  22389  limcres  22394  lhop1  22519  dvdsr1p  22666  fsumvma2  23625  vmasum  23627  chpchtsum  23630  bposlem1  23695  iscgrgd  24046  lnrot1  24144  eqeelen  24349  nbgraeledg  24572  nb3graprlem2  24594  cusgra3v  24606  cusgrauvtxb  24638  clwlkisclwwlk2  24932  el2spthonot0  25013  rusgranumwlks  25098  dmdmd  27356  funcnvmptOLD  27685  funcnvmpt  27686  1stpreimas  27701  xrdifh  27774  ismntop  28188  eulerpartlemgh  28536  signslema  28738  leceifl  30245  iblabsnclem  30280  ftc1anclem6  30297  areacirclem5  30313  areacirc  30314  ellz1  30901  islssfg  31218  proot1ex  31365  eliooshift  31742  clim2cf  31857  odd2np1ALTV  32551  lsatfixedN  35182  cdlemg10c  36813  diaglbN  37230  dih1  37461  dihglbcpreN  37475  mapdcv  37835