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  3054  sbcnel12g  3110  elxp4  5171  elxp5  5172  f1eq123d  5516  foeq123d  5517  f1oeq123d  5518  fnmptfvd  5686  ofrfval  6169  eloprabi  6284  fnmpoovd  6303  smoeq  6378  ecidg  6688  ixpsnval  6790  enqbreq2  7472  ltanqg  7515  caucvgprprlemexb  7822  caucvgsrlemgt1  7910  caucvgsrlemoffres  7915  ltrennb  7969  apneg  8686  mulext1  8687  apdivmuld  8888  ltdiv23  8967  lediv23  8968  halfpos  9270  addltmul  9276  div4p1lem1div2  9293  ztri3or  9417  supminfex  9720  iccf1o  10128  fzshftral  10232  fzoshftral  10369  infssuzex  10378  2tnp1ge0ge0  10446  fihashen1  10946  seq3coll  10989  s111  11088  swrdspsleq  11123  pfxeq  11150  cjap  11250  negfi  11572  tanaddaplem  12082  dvdssub  12182  addmodlteqALT  12203  dvdsmod  12206  oddp1even  12220  nn0o1gt2  12249  nn0oddm1d2  12253  bitscmp  12302  cncongr1  12458  cncongr2  12459  4sqlem11  12757  4sqlem17  12763  intopsn  13232  sgrp1  13276  sgrppropd  13278  issubg  13542  nmzsubg  13579  conjnmzb  13649  srg1zr  13782  ring1  13854  issubrg  14016  znf1o  14446  znleval  14448  znunit  14454  elmopn  14951  metss  14999  comet  15004  xmetxp  15012  limcmpted  15168  cnlimc  15177  lgsneg  15534  lgsne0  15548  lgsprme0  15552  lgsquadlem1  15587  lgsquadlem2  15588  2lgs  15614  2lgsoddprm  15623  edg0iedg0g  15693