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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sbceqal  3107  sbcnel12g  3164  elxp4  5278  elxp5  5279  f1eq123d  5634  foeq123d  5635  f1oeq123d  5636  fnmptfvd  5816  ofrfval  6315  eloprabi  6436  fnmpoovd  6455  suppsnopdc  6494  smoeq  6565  ecidg  6877  ixpsnval  6987  mapsnend  7103  enqbreq2  7730  ltanqg  7773  caucvgprprlemexb  8080  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  ltrennb  8227  apneg  8947  mulext1  8948  apdivmuld  9151  ltdiv23  9230  lediv23  9231  halfpos  9547  addltmul  9553  div4p1lem1div2  9570  ztri3or  9698  supminfex  10013  iccf1o  10424  fzsplit3  10475  fzshftral  10532  fzoshftral  10674  infssuzex  10683  2tnp1ge0ge0  10757  fihashen1  11260  seq3coll  11316  s111  11421  swrdspsleq  11461  pfxeq  11490  wrd2ind  11517  cjap  11694  negfi  12017  tanaddaplem  12530  dvdssub  12630  addmodlteqALT  12651  dvdsmod  12654  oddp1even  12668  nn0o1gt2  12697  nn0oddm1d2  12701  bitscmp  12750  cncongr1  12906  cncongr2  12907  4sqlem11  13209  4sqlem17  13215  ballotfilemsima  13317  intopsn  13746  sgrp1  13785  sgrppropd  13787  issubg  14035  nmzsubg  14072  conjnmzb  14142  rng1zrlem  14365  ring1  14471  issubrg  14638  znf1o  15095  znleval  15097  znunit  15103  elmopn  15672  metss  15720  comet  15725  xmetxp  15733  limcmpted  15889  cnlimc  15898  sineq0re  16076  chtqub  16296  bposlem7  16317  lgsneg  16348  lgsne0  16362  lgsprme0  16366  lgsquadlem1  16401  lgsquadlem2  16402  2lgs  16428  2lgsoddprm  16437  edg0iedg0g  16512  wrdupgren  16542  wrdumgren  16552  vtxd0nedgbfi  16745  eupth2lem2dc  16905  eupth2lem3lem6fi  16917  eupth2lem3lem4fi  16919