Theorem 3bitrd 213

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sbceqal  2964  sbcnel12g  3019  elxp4  5026  elxp5  5027  f1eq123d  5360  foeq123d  5361  f1oeq123d  5362  ofrfval  5990  eloprabi  6094  fnmpoovd  6112  smoeq  6187  ecidg  6493  ixpsnval  6595  enqbreq2  7165  ltanqg  7208  caucvgprprlemexb  7515  caucvgsrlemgt1  7603  caucvgsrlemoffres  7608  ltrennb  7662  apneg  8373  mulext1  8374  apdivmuld  8573  ltdiv23  8650  lediv23  8651  halfpos  8951  addltmul  8956  div4p1lem1div2  8973  ztri3or  9097  supminfex  9392  iccf1o  9787  fzshftral  9888  fzoshftral  10015  2tnp1ge0ge0  10074  fihashen1  10545  seq3coll  10585  cjap  10678  negfi  10999  tanaddaplem  11445  dvdssub  11538  addmodlteqALT  11557  dvdsmod  11560  oddp1even  11573  nn0o1gt2  11602  nn0oddm1d2  11606  infssuzex  11642  cncongr1  11784  cncongr2  11785  elmopn  12615  metss  12663  comet  12668  xmetxp  12676  limcmpted  12801  cnlimc  12810