Theorem 3bitrd 279

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  sbceqal  3329  elimhyp3v  3945  elimhyp4v  3946  keephyp3v  3951  opelopabgf  4710  elpredg  5381  f1eq123d  5794  foeq123d  5795  f1oeq123d  5796  fnmptfvd  5968  ofrfval  6529  eloprabi  6846  fnmpt2ovd  6862  suppsnop  6916  smoeq  7054  wemapwe  8171  wemapweOLD  8172  fseqenlem1  8437  dfac12lem2  8556  fin23lem22  8739  pwfseqlem5  9071  pwfseq  9072  enqbreq2  9328  lterpq  9378  ltdiv23  10476  lediv23  10477  halfpos  10810  addltmul  10815  supminf  11214  supxrbnd1  11566  supxrbnd2  11567  iccf1o  11718  fzshftral  11821  fzoshftral  11960  dfceil2  12006  modirr  12098  hashen1  12487  seqcoll  12561  s111  12677  swrdeq  12725  wrd2ind  12759  2swrd2eqwrdeq  12947  limsupgle  13449  tanaddlem  14110  dvdssub  14235  dvdsmod  14252  oddp1even  14257  bitscmp  14297  saddisjlem  14323  smueqlem  14349  prmreclem5  14647  4sqlem11  14682  4sqlem17  14688  vdwmc2  14706  ismre  15204  acsfn  15273  dfiso2  15385  brcic  15411  isssc  15433  setcinv  15693  intopsn  16206  sgrp1  16242  mnd1OLD  16286  sgrp2nmndlem4  16370  nmzsubg  16566  conjnmzb  16625  gsmsymgreqlem2  16780  symgfixels  16783  f1omvdconj  16795  oddvdsnn0  16892  oddvds  16895  odcong  16897  odf1  16908  dpjeq  17428  dpjeqOLD  17435  pgpfac1lem2  17446  ring1  17568  lsmspsn  18050  lbsacsbs  18122  lpigen  18224  prmirredlem  18830  znf1o  18888  znleval  18891  znunit  18900  islinds2  19140  islindf4  19165  scmatf1  19325  isclo  19881  maxlp  19941  1stccn  20256  xkoinjcn  20480  elmptrab  20620  fbunfip  20662  elfm  20740  fmid  20753  flfnei  20784  isflf  20786  isfcls  20802  fclsopn  20807  isfcf  20827  cnextfun  20856  eltsms  20923  prdsxmetlem  21163  elmopn  21237  metss  21303  comet  21308  elbl4  21371  metuel2  21374  nrmmetd  21387  metdsge  21645  tchcph  21972  fmcfil  22003  rrxmet  22127  minveclem4  22139  shft2rab  22211  sca2rab  22215  volsup2  22306  mbfsup  22363  i1fmullem  22393  mbfi1fseqlem4  22417  xrge0f  22430  itg2monolem1  22449  ellimc2  22573  cnlimc  22584  mdegleb  22756  facth1  22857  ulm2  23072  sineq0  23206  coseq1  23207  efeq1  23208  sinord  23213  root1eq1  23425  angrtmuld  23467  quad2  23495  dcubic  23502  cubic2  23504  dquartlem1  23507  dquart  23509  quart  23517  rlimcnp  23621  lgamucov  23693  mumullem2  23835  chtub  23868  fsumvma  23869  fsumvma2  23870  chpchtsum  23875  bposlem7  23946  lgsneg  23975  lgsne0  23989  lgsqrlem2  23998  lgsquadlem1  24010  lgsquadlem2  24011  istrkg3ld  24237  axcontlem7  24690  isuslgra  24760  isusgra  24761  ausisusgra  24772  nbgraopALT  24841  nb3graprlem2  24869  cusgra3v  24881  sizeusglecusg  24903  uvtx01vtx  24909  is2wlk  24984  0pth  24989  wlkdvspthlem  25026  2wlkeq  25124  wwlknextbi  25142  clwwlkn2  25192  el2wlkonotot0  25289  el2wlkonotot  25290  el2wlksoton  25295  el2spthsoton  25296  el2wlksot  25297  el2pthsot  25298  isrusgusrgcl  25350  rusgrasn  25362  rusgranumwlkl1  25364  rusgra0edg  25372  eupath2lem2  25395  eupath2lem3  25396  frgra2v  25416  frgra3v  25419  usg2spot2nb  25482  numclwwlkovfel2  25500  numclwwlk2lem1  25519  numclwlk2lem2f1o  25522  frgrareggt1  25533  isass  25732  rngosn3  25842  imsmetlem  26010  ipz  26046  bnsscmcl  26198  minvecolem4  26210  hvsubcan  26405  hoeq2  27163  leoptri  27468  atcv0eq  27711  elimifd  27842  gtiso  27963  2ndpreima  27970  fpwrelmapffslem  28002  fzsplit3  28047  isomnd  28143  ogrpinvlt  28166  pstmfval  28328  lmlim  28382  dya2ub  28718  eulerpartlemr  28819  isrrvv  28888  ballotlemsima  28960  signsvfn  29045  subfacp1lem3  29479  subfacp1lem5  29481  erdszelem1  29488  erdsze  29499  erdsze2lem2  29501  filnetlem4  30609  bj-issetwt  30999  bj-sbceqgALT  31033  dvtanlemOLD  31437  itg2addnclem2  31440  ftc1anclem1  31463  areacirclem1  31478  areacirclem5  31482  metf1o  31530  lsatcv0eq  32065  cmtbr2N  32271  atlatmstc  32337  1cvrco  32489  cdleme3  33255  cdleme7  33267  cdlemg10c  33658  dvhopellsm  34137  dibord  34179  dib1dim2  34188  diblsmopel  34191  dihopelvalcpre  34268  dih1dimatlem  34349  hdmap14lem13  34903  hdmapoc  34954  elrfirn  34989  jm2.19lem2  35294  pwfi2f1o  35406  proot1ex  35525  brfvidRP  35667  bcc0  36093  fourierdlem113  37370  2reu4a  37562  iccpartgtl  37693  iccpartleu  37695  iccpartgel  37696  bits0ALTV  37761  bgoldbtbndlem1  37853  pfxeq  37891  ltnltne  37953  0nodd  38127  2nodd  38129  rngcinv  38300  rngcinvALTV  38312  ringcinv  38351  ringcinvALTV  38375  islindeps  38565  snlindsntor  38583  nn0o1gt2  38647  blen1b  38719  nn0sumshdiglem1  38752