Theorem 3bitr4rd 290

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

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

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 189

This theorem is referenced by:  inimasn  5256  oacan  7254  ecdmn0  7411  wemapwe  8207  r1pw  8321  adderpqlem  9384  mulerpqlem  9385  lterpq  9400  ltanq  9401  genpass  9439  readdcan  9812  lemuldiv  10493  msq11  10514  avglt2  10858  qbtwnre  11499  iooshf  11720  clim2c  13581  lo1o1  13608  climabs0  13661  reef11  14185  absefib  14264  efieq1re  14265  pc2dvds  14840  pcmpt  14849  subsubc  15770  odmulgid  17217  gexdvds  17247  submcmn2  17491  obslbs  19305  cnntr  20303  cndis  20319  cnindis  20320  cnpdis  20321  lmres  20328  cmpfi  20435  ist0-4  20756  txhmeo  20830  tsmssubm  21169  blin  21448  cncfmet  21952  icopnfcnv  21982  lmmbrf  22244  iscauf  22262  causs  22280  mbfposr  22620  itg2gt0  22730  limcflf  22848  limcres  22853  lhop1  22978  dvdsr1p  23124  fsumvma2  24154  vmasum  24156  chpchtsum  24159  bposlem1  24224  iscgrgd  24570  tgcgr4  24588  lnrot1  24680  eqeelen  24946  nbgraeledg  25170  nb3graprlem2  25192  cusgra3v  25204  cusgrauvtxb  25236  clwlkisclwwlk2  25530  el2spthonot0  25611  rusgranumwlks  25696  dmdmd  27965  funcnvmptOLD  28282  funcnvmpt  28283  1stpreimas  28298  xrdifh  28374  ismntop  28842  eulerpartlemgh  29223  signslema  29463  topdifinfindis  31761  leceifl  31946  iblabsnclem  32017  ftc1anclem6  32034  areacirclem5  32048  areacirc  32049  lsatfixedN  32587  cdlemg10c  34218  diaglbN  34635  dih1  34866  dihglbcpreN  34880  mapdcv  35240  ellz1  35621  islssfg  35940  proot1ex  36090  eliooshift  37614  clim2cf  37741  odd2np1ALTV  38813  nbusgreledg  39431  nb3grprlem2  39465