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  5275  elxp5  5276  f1eq123d  5631  foeq123d  5632  f1oeq123d  5633  fnmptfvd  5813  ofrfval  6311  eloprabi  6432  fnmpoovd  6451  suppsnopdc  6490  smoeq  6561  ecidg  6873  ixpsnval  6983  mapsnend  7099  enqbreq2  7725  ltanqg  7768  caucvgprprlemexb  8075  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  ltrennb  8222  apneg  8942  mulext1  8943  apdivmuld  9146  ltdiv23  9225  lediv23  9226  halfpos  9541  addltmul  9547  div4p1lem1div2  9564  ztri3or  9692  supminfex  10007  iccf1o  10418  fzsplit3  10469  fzshftral  10526  fzoshftral  10668  infssuzex  10677  2tnp1ge0ge0  10751  fihashen1  11254  seq3coll  11310  s111  11415  swrdspsleq  11455  pfxeq  11484  wrd2ind  11511  cjap  11688  negfi  12011  tanaddaplem  12524  dvdssub  12624  addmodlteqALT  12645  dvdsmod  12648  oddp1even  12662  nn0o1gt2  12691  nn0oddm1d2  12695  bitscmp  12744  cncongr1  12900  cncongr2  12901  4sqlem11  13203  4sqlem17  13209  ballotfilemsima  13311  intopsn  13740  sgrp1  13779  sgrppropd  13781  issubg  14029  nmzsubg  14066  conjnmzb  14136  rng1zrlem  14342  ring1  14448  issubrg  14613  znf1o  15070  znleval  15072  znunit  15078  elmopn  15638  metss  15686  comet  15691  xmetxp  15699  limcmpted  15855  cnlimc  15864  chtqub  16257  bposlem7  16278  lgsneg  16309  lgsne0  16323  lgsprme0  16327  lgsquadlem1  16362  lgsquadlem2  16363  2lgs  16389  2lgsoddprm  16398  edg0iedg0g  16473  wrdupgren  16503  wrdumgren  16513  vtxd0nedgbfi  16706  eupth2lem2dc  16866  eupth2lem3lem6fi  16878  eupth2lem3lem4fi  16880