Theorem 3bitrd 283

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

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

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 189

This theorem is referenced by:  sbceqal  3319  elimhyp3v  3941  elimhyp4v  3942  keephyp3v  3947  opelopabgf  4721  elpredg  5394  f1eq123d  5809  foeq123d  5810  f1oeq123d  5811  fnmptfvd  5985  ofrfval  6539  eloprabi  6855  fnmpt2ovd  6871  suppsnop  6928  smoeq  7069  infglbb  8007  wemapwe  8202  fseqenlem1  8455  dfac12lem2  8574  fin23lem22  8757  pwfseqlem5  9088  pwfseq  9089  enqbreq2  9345  lterpq  9395  ltdiv23  10497  lediv23  10498  negfi  10554  halfpos  10843  addltmul  10848  supminf  11250  supminfOLD  11251  supxrbnd1  11607  supxrbnd2  11608  iccf1o  11776  fzshftral  11882  fzoshftral  12022  dfceil2  12068  modirr  12160  hashen1  12550  seqcoll  12627  hash2prb  12633  s111  12752  swrdeq  12800  wrd2ind  12834  2swrd2eqwrdeq  13028  limsupgle  13535  tanaddlem  14220  dvdssub  14345  dvdsmod  14362  oddp1even  14367  bitscmp  14412  saddisjlem  14438  smueqlem  14464  ncoprmgcdne1b  14655  prmreclem5  14864  4sqlem11  14899  4sqlem17OLD  14905  4sqlem17  14911  vdwmc2  14929  ismre  15496  acsfn  15565  dfiso2  15677  brcic  15703  isssc  15725  setcinv  15985  intopsn  16498  sgrp1  16534  mnd1OLD  16578  sgrp2nmndlem4  16662  nmzsubg  16858  conjnmzb  16917  gsmsymgreqlem2  17072  symgfixels  17075  f1omvdconj  17087  oddvdsnn0  17193  oddvds  17196  odcong  17198  odf1  17213  dpjeq  17692  pgpfac1lem2  17708  ring1  17830  lsmspsn  18307  lbsacsbs  18379  lpigen  18480  prmirredlem  19064  znf1o  19122  znleval  19125  znunit  19134  islinds2  19371  islindf4  19396  scmatf1  19556  isclo  20103  maxlp  20163  1stccn  20478  xkoinjcn  20702  elmptrab  20842  fbunfip  20884  elfm  20962  fmid  20975  flfnei  21006  isflf  21008  isfcls  21024  fclsopn  21029  isfcf  21049  cnextfun  21079  eltsms  21147  prdsxmetlem  21383  elmopn  21457  metss  21523  comet  21528  elbl4  21578  metuel2  21580  nrmmetd  21589  metdsge  21866  metdsgeOLD  21881  tchcph  22211  fmcfil  22242  rrxmet  22362  minveclem4  22374  minveclem4OLD  22386  shft2rab  22461  sca2rab  22465  volsup2  22563  mbfsup  22620  i1fmullem  22652  mbfi1fseqlem4  22676  xrge0f  22689  itg2monolem1  22708  ellimc2  22832  cnlimc  22843  mdegleb  23013  facth1  23115  ulm2  23340  sineq0  23476  coseq1  23477  efeq1  23478  sinord  23483  root1eq1  23695  angrtmuld  23737  quad2  23765  dcubic  23772  cubic2  23774  dquartlem1  23777  dquart  23779  quart  23787  rlimcnp  23891  lgamucov  23963  mumullem2  24107  chtub  24140  fsumvma  24141  fsumvma2  24142  chpchtsum  24147  bposlem7  24218  lgsneg  24247  lgsne0  24261  lgsqrlem2  24270  lgsquadlem1  24282  lgsquadlem2  24283  istrkg3ld  24509  tgcgr4  24576  iscgra1  24852  isleag  24883  iseqlg  24897  axcontlem7  25000  isuslgra  25070  isusgra  25071  ausisusgra  25082  nbgraopALT  25152  nb3graprlem2  25180  cusgra3v  25192  sizeusglecusg  25214  uvtx01vtx  25220  is2wlk  25295  0pth  25300  wlkdvspthlem  25337  2wlkeq  25435  wwlknextbi  25453  clwwlkn2  25503  el2wlkonotot0  25600  el2wlkonotot  25601  el2wlksoton  25606  el2spthsoton  25607  el2wlksot  25608  el2pthsot  25609  isrusgusrgcl  25661  rusgrasn  25673  rusgranumwlkl1  25675  rusgra0edg  25683  eupath2lem2  25706  eupath2lem3  25707  frgra2v  25727  frgra3v  25730  usg2spot2nb  25793  numclwwlkovfel2  25811  numclwwlk2lem1  25830  numclwlk2lem2f1o  25833  frgrareggt1  25844  isass  26044  rngosn3  26154  imsmetlem  26322  ipz  26358  bnsscmcl  26510  minvecolem4  26522  minvecolem4OLD  26532  hvsubcan  26727  hoeq2  27484  leoptri  27789  atcv0eq  28032  elimifd  28160  gtiso  28281  2ndpreima  28288  fpwrelmapffslem  28317  fzsplit3  28370  isomnd  28464  ogrpinvlt  28487  smatrcl  28622  pstmfval  28699  lmlim  28753  dya2ub  29092  eulerpartlemr  29207  isrrvv  29276  ballotlemsima  29348  ballotlemsimaOLD  29386  signsvfn  29471  subfacp1lem3  29905  subfacp1lem5  29907  erdszelem1  29914  erdsze  29925  erdsze2lem2  29927  filnetlem4  31037  bj-issetwt  31468  bj-sbceqgALT  31504  csbwrecsg  31728  poimirlem24  31964  dvtanlemOLD  31991  itg2addnclem2  31994  ftc1anclem1  32017  areacirclem1  32032  areacirclem5  32036  metf1o  32084  lsatcv0eq  32613  cmtbr2N  32819  atlatmstc  32885  1cvrco  33037  cdleme3  33803  cdleme7  33815  cdlemg10c  34206  dvhopellsm  34685  dibord  34727  dib1dim2  34736  diblsmopel  34739  dihopelvalcpre  34816  dih1dimatlem  34897  hdmap14lem13  35451  hdmapoc  35502  elrfirn  35537  jm2.19lem2  35845  pwfi2f1o  35954  proot1ex  36078  brfvidRP  36280  bcc0  36689  pwpwuni  37397  rnmptpr  37444  disjinfi  37468  mapsnend  37480  fourierdlem113  38083  2reu4a  38610  iccpartgtl  38740  iccpartleu  38742  iccpartgel  38743  bits0ALTV  38808  bgoldbtbndlem1  38900  pfxeq  38945  ltnltne  39045  edg0iedg0  39218  ausgrusgrb  39252  nb3grprlem2  39455  uvtxa01vtx0  39469  cplgr3v  39502  uhgrvd0nedgb  39545  vtxdusgr0edgnelALT  39550  upgr2wlk  39664  0nodd  39863  2nodd  39865  rngcinv  40036  rngcinvALTV  40048  ringcinv  40087  ringcinvALTV  40111  islindeps  40299  snlindsntor  40317  nn0o1gt2  40380  blen1b  40452  nn0sumshdiglem1  40485