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  5421  oacan  7194  ecdmn0  7351  wemapwe  8135  wemapweOLD  8136  r1pw  8259  adderpqlem  9328  mulerpqlem  9329  lterpq  9344  ltanq  9345  genpass  9383  readdcan  9749  lemuldiv  10420  msq11  10442  avglt2  10773  qbtwnre  11394  iooshf  11599  clim2c  13287  lo1o1  13314  climabs0  13367  reef11  13711  absefib  13790  efieq1re  13791  pc2dvds  14257  pcmpt  14266  subsubc  15076  odmulgid  16372  gexdvds  16400  submcmn2  16640  obslbs  18528  cnntr  19542  cndis  19558  cnindis  19559  cnpdis  19560  lmres  19567  cmpfi  19674  ist0-4  19965  txhmeo  20039  tsmssubm  20379  blin  20659  cncfmet  21147  icopnfcnv  21177  lmmbrf  21436  iscauf  21454  causs  21472  mbfposr  21794  itg2gt0  21902  limcflf  22020  limcres  22025  lhop1  22150  dvdsr1p  22297  fsumvma2  23217  vmasum  23219  chpchtsum  23222  bposlem1  23287  iscgrgd  23633  lnrot1  23717  eqeelen  23883  nbgraeledg  24106  nb3graprlem2  24128  cusgra3v  24140  cusgrauvtxb  24172  clwlkisclwwlk2  24466  el2spthonot0  24547  rusgranumwlks  24632  dmdmd  26895  funcnvmptOLD  27181  funcnvmpt  27182  xrdifh  27259  ismntop  27644  eulerpartlemgh  27957  signslema  28159  leceifl  29621  iblabsnclem  29655  ftc1anclem6  29672  areacirclem5  29688  areacirc  29689  ellz1  30304  islssfg  30620  proot1ex  30766  clim2cf  31192  lsatfixedN  33806  cdlemg10c  35435  diaglbN  35852  dih1  36083  dihglbcpreN  36097  mapdcv  36457