Theorem 3bitr4rd 294

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 264	. 2 |- ( ph -> ( ta <-> ps ) )
4		3bitr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
5	3, 4	bitr4d 264	1 |- ( ph -> ( ta <-> th ) )

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

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 190

This theorem is referenced by:  inimasn  5259  oacan  7267  ecdmn0  7424  wemapwe  8220  r1pw  8334  adderpqlem  9397  mulerpqlem  9398  lterpq  9413  ltanq  9414  genpass  9452  readdcan  9825  lemuldiv  10508  msq11  10529  avglt2  10874  qbtwnre  11515  iooshf  11738  clim2c  13646  lo1o1  13673  climabs0  13726  reef11  14250  absefib  14329  efieq1re  14330  pc2dvds  14907  pcmpt  14916  subsubc  15836  odmulgid  17283  gexdvds  17313  submcmn2  17557  obslbs  19370  cnntr  20368  cndis  20384  cnindis  20385  cnpdis  20386  lmres  20393  cmpfi  20500  ist0-4  20821  txhmeo  20895  tsmssubm  21235  blin  21514  cncfmet  22018  icopnfcnv  22048  lmmbrf  22310  iscauf  22328  causs  22346  mbfposr  22687  itg2gt0  22797  limcflf  22915  limcres  22920  lhop1  23045  dvdsr1p  23191  fsumvma2  24221  vmasum  24223  chpchtsum  24226  bposlem1  24291  iscgrgd  24637  tgcgr4  24655  lnrot1  24747  eqeelen  25013  nbgraeledg  25237  nb3graprlem2  25259  cusgra3v  25271  cusgrauvtxb  25303  clwlkisclwwlk2  25597  el2spthonot0  25678  rusgranumwlks  25763  dmdmd  28034  funcnvmptOLD  28345  funcnvmpt  28346  1stpreimas  28361  xrdifh  28437  ismntop  28904  eulerpartlemgh  29284  signslema  29523  topdifinfindis  31819  leceifl  31998  iblabsnclem  32069  ftc1anclem6  32086  areacirclem5  32100  areacirc  32101  lsatfixedN  32646  cdlemg10c  34277  diaglbN  34694  dih1  34925  dihglbcpreN  34939  mapdcv  35299  ellz1  35680  islssfg  35999  proot1ex  36149  eliooshift  37700  clim2cf  37828  odd2np1ALTV  38948  nbusgreledg  39585  nb3grprlem2  39619