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  5242  oacan  6975  ecdmn0  7131  wemapwe  7916  wemapweOLD  7917  r1pw  8040  adderpqlem  9110  mulerpqlem  9111  lterpq  9126  ltanq  9127  genpass  9165  readdcan  9530  lemuldiv  10198  msq11  10220  avglt2  10550  qbtwnre  11156  iooshf  11361  clim2c  12966  lo1o1  12993  climabs0  13046  reef11  13385  absefib  13464  efieq1re  13465  pc2dvds  13927  pcmpt  13936  subsubc  14745  odmulgid  16034  gexdvds  16062  submcmn2  16302  obslbs  17996  cnntr  18720  cndis  18736  cnindis  18737  cnpdis  18738  lmres  18745  cmpfi  18852  ist0-4  19143  txhmeo  19217  tsmssubm  19557  blin  19837  cncfmet  20325  icopnfcnv  20355  lmmbrf  20614  iscauf  20632  causs  20650  mbfposr  20971  itg2gt0  21079  limcflf  21197  limcres  21202  lhop1  21327  dvdsr1p  21517  fsumvma2  22437  vmasum  22439  chpchtsum  22442  bposlem1  22507  iscgrgd  22846  lnrot1  22903  eqeelen  22972  nbgraeledg  23163  nb3graprlem2  23182  cusgra3v  23194  cusgrauvtxb  23226  dmdmd  25526  funcnvmptOLD  25809  funcnvmpt  25810  xrdifh  25892  eulerpartlemgh  26608  signslema  26810  leceifl  28261  iblabsnclem  28296  ftc1anclem6  28313  areacirclem5  28329  areacirc  28330  ellz1  28947  islssfg  29265  proot1ex  29411  el2spthonot0  30233  clwlkisclwwlk2  30295  rusgranumwlks  30417  lsatfixedN  32224  cdlemg10c  33853  diaglbN  34270  dih1  34501  dihglbcpreN  34515  mapdcv  34875