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  6566  ecidg  6878  ixpsnval  6989  mapsnend  7105  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  9696  supminfex  10012  iccf1o  10423  fzsplit3  10474  fzshftral  10531  fzoshftral  10673  infssuzex  10682  2tnp1ge0ge0  10756  fihashen1  11259  seq3coll  11315  s111  11420  swrdspsleq  11460  pfxeq  11489  wrd2ind  11516  cjap  11693  negfi  12016  tanaddaplem  12529  dvdssub  12629  addmodlteqALT  12650  dvdsmod  12653  oddp1even  12667  nn0o1gt2  12696  nn0oddm1d2  12700  bitscmp  12749  cncongr1  12905  cncongr2  12906  4sqlem11  13208  4sqlem17  13214  ballotfilemsima  13316  intopsn  13745  sgrp1  13784  sgrppropd  13786  issubg  14034  nmzsubg  14071  conjnmzb  14141  rng1zrlem  14364  ring1  14470  issubrg  14637  znf1o  15094  znleval  15096  znunit  15102  elmopn  15689  metss  15737  comet  15742  xmetxp  15750  limcmpted  15906  cnlimc  15915  sineq0re  16093  chtqub  16313  bposlem7  16334  lgsneg  16365  lgsne0  16379  lgsprme0  16383  lgsquadlem1  16418  lgsquadlem2  16419  2lgs  16445  2lgsoddprm  16454  edg0iedg0g  16529  wrdupgren  16559  wrdumgren  16569  vtxd0nedgbfi  16762  eupth2lem2dc  16922  eupth2lem3lem6fi  16934  eupth2lem3lem4fi  16936