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  5361  oacan  7096  ecdmn0  7252  wemapwe  8038  wemapweOLD  8039  r1pw  8162  adderpqlem  9233  mulerpqlem  9234  lterpq  9249  ltanq  9250  genpass  9288  readdcan  9653  lemuldiv  10321  msq11  10343  avglt2  10673  qbtwnre  11279  iooshf  11484  clim2c  13100  lo1o1  13127  climabs0  13180  reef11  13520  absefib  13599  efieq1re  13600  pc2dvds  14062  pcmpt  14071  subsubc  14881  odmulgid  16175  gexdvds  16203  submcmn2  16443  obslbs  18279  cnntr  19010  cndis  19026  cnindis  19027  cnpdis  19028  lmres  19035  cmpfi  19142  ist0-4  19433  txhmeo  19507  tsmssubm  19847  blin  20127  cncfmet  20615  icopnfcnv  20645  lmmbrf  20904  iscauf  20922  causs  20940  mbfposr  21262  itg2gt0  21370  limcflf  21488  limcres  21493  lhop1  21618  dvdsr1p  21765  fsumvma2  22685  vmasum  22687  chpchtsum  22690  bposlem1  22755  iscgrgd  23101  lnrot1  23167  eqeelen  23301  nbgraeledg  23492  nb3graprlem2  23511  cusgra3v  23523  cusgrauvtxb  23555  dmdmd  25855  funcnvmptOLD  26136  funcnvmpt  26137  xrdifh  26214  eulerpartlemgh  26904  signslema  27106  leceifl  28567  iblabsnclem  28602  ftc1anclem6  28619  areacirclem5  28635  areacirc  28636  ellz1  29252  islssfg  29570  proot1ex  29716  el2spthonot0  30537  clwlkisclwwlk2  30599  rusgranumwlks  30721  lsatfixedN  32977  cdlemg10c  34606  diaglbN  35023  dih1  35254  dihglbcpreN  35268  mapdcv  35628