Theorem 3bitrd 214

Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)

Hypotheses

Ref	Expression
3bitrd.1	|- ( ph -> ( ps <-> ch ) )
3bitrd.2	|- ( ph -> ( ch <-> th ) )
3bitrd.3	|- ( ph -> ( th <-> ta ) )

Assertion

Ref	Expression
3bitrd	|- ( ph -> ( ps <-> ta ) )

Proof of Theorem 3bitrd

Step	Hyp	Ref	Expression
1		3bitrd.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		3bitrd.2	. . 3 |- ( ph -> ( ch <-> th ) )
3	1, 2	bitrd 188	. 2 |- ( ph -> ( ps <-> th ) )
4		3bitrd.3	. 2 |- ( ph -> ( th <-> ta ) )
5	3, 4	bitrd 188	1 |- ( ph -> ( ps <-> ta ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sbceqal  3042  sbcnel12g  3098  elxp4  5154  elxp5  5155  f1eq123d  5493  foeq123d  5494  f1oeq123d  5495  fnmptfvd  5663  ofrfval  6141  eloprabi  6251  fnmpoovd  6270  smoeq  6345  ecidg  6655  ixpsnval  6757  enqbreq2  7419  ltanqg  7462  caucvgprprlemexb  7769  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  ltrennb  7916  apneg  8632  mulext1  8633  apdivmuld  8834  ltdiv23  8913  lediv23  8914  halfpos  9216  addltmul  9222  div4p1lem1div2  9239  ztri3or  9363  supminfex  9665  iccf1o  10073  fzshftral  10177  fzoshftral  10308  2tnp1ge0ge0  10373  fihashen1  10873  seq3coll  10916  cjap  11053  negfi  11374  tanaddaplem  11884  dvdssub  11984  addmodlteqALT  12004  dvdsmod  12007  oddp1even  12020  nn0o1gt2  12049  nn0oddm1d2  12053  infssuzex  12089  cncongr1  12244  cncongr2  12245  4sqlem11  12542  4sqlem17  12548  intopsn  12953  sgrp1  12997  sgrppropd  12999  issubg  13246  nmzsubg  13283  conjnmzb  13353  srg1zr  13486  ring1  13558  issubrg  13720  znf1o  14150  znleval  14152  znunit  14158  elmopn  14625  metss  14673  comet  14678  xmetxp  14686  limcmpted  14842  cnlimc  14851  lgsneg  15181  lgsne0  15195  lgsprme0  15199  lgsquadlem1  15234  lgsquadlem2  15235  2lgs  15261  2lgsoddprm  15270