Theorem syl5bb 257

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl5bb.1	|- ( ph <-> ps )
syl5bb.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5bb	|- ( ch -> ( ph <-> th ) )

Proof of Theorem syl5bb

Step	Hyp	Ref	Expression
1		syl5bb.1	. . 3 |- ( ph <-> ps )
2	1	a1i 11	. 2 |- ( ch -> ( ph <-> ps ) )
3		syl5bb.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	bitrd 253	1 |- ( ch -> ( ph <-> th ) )

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:  syl5rbb  258  syl5bbr  259  3bitr4g  288  imim21b  367  cad0  1442  had1  1444  ax12wdemo  1769  sbal2  2173  abbi  2548  necon3abid  2636  necon3bid  2638  necon1abid  2659  r19.21t  2796  ceqsralt  2991  ralxpxfr2d  3079  ceqsrexv  3088  ceqsrex2v  3090  elab2g  3103  elrabf  3110  eueq2  3128  eqreu  3146  reu8  3150  ru  3180  sbcralt  3262  sbcabel  3270  sbcel1g  3676  sbcel2  3678  csbnestgf  3687  sbccsb2  3698  disjpss  3724  sbcssg  3785  rexsng  3908  ralprg  3920  rexprg  3921  difsn  4003  opthpr  4045  ralunsn  4074  csbuni  4114  dfiin2g  4198  iunxsng  4244  elpwuni  4253  disjxun  4285  sbcbr12g  4341  pwnss  4452  opthneg  4566  opelopabt  4596  opelopabga  4597  brabga  4598  csbmpt12  4617  dfid3  4632  frirr  4692  wereu2  4712  ordtri4  4751  oneqmini  4765  elsucg  4781  elsuc2g  4782  brab2a  4883  opeliunxp  4885  posn  4902  sosn  4903  frsn  4904  brab2ga  4907  opbrop  4911  csbcnvgALT  5019  elrnmpt1  5083  elrnmptg  5084  eliniseg2  5203  poleloe  5227  xpdifid  5261  cnvpo  5370  sbcfung  5436  dffun8  5440  fncnv  5477  fununi  5479  fnssresb  5518  fnimaeq0  5527  funcocnv2  5660  csbfv12  5720  dffn5  5732  funimass4  5737  fnsnfv  5746  dmfco  5760  fndmdif  5802  fvimacnvi  5812  fvimacnvALT  5817  unpreima  5824  respreima  5827  fmptco  5871  fressnfv  5891  fnnfpeq0  5904  fnsuppresOLD  5933  elunirn  5963  dff13  5966  fliftel  5997  isoini  6024  f1oiso  6037  eloprabga  6172  resoprab2  6182  elrnmpt2res  6199  ralrnmpt2  6200  ovid  6202  ov  6205  ovg  6224  ofrfval2  6332  dfwe2  6388  ssonprc  6398  ordpwsuc  6421  dfom2  6473  f1oweALT  6556  fmpt2x  6635  ovmptss  6649  1stconst  6656  2ndconst  6657  fnsuppres  6711  isprmpt2  6738  brtpos2  6746  dfsmo2  6800  rdglim2  6880  seqomlem2  6898  omeu  7016  oeeui  7033  brdifun  7120  eqerlem  7125  brecop  7185  erovlem  7188  eceqoveq  7197  mapsn  7246  ixpsnval  7258  mptelixpg  7292  map1  7380  xpsnen  7387  xpdom2  7398  omxpenlem  7404  xpf1o  7465  mapunen  7472  onfin  7493  fimaxg  7551  fodomfib  7583  fofinf1o  7584  fipreima  7609  supub  7701  ordtypecbv  7723  ordtypelem3  7726  ordtypelem9  7732  hartogslem1  7748  wofib  7751  wemapsolem  7756  wemapso2OLD  7758  wemapso2lem  7759  noinfep  7857  noinfepOLD  7858  cantnf  7893  cantnfOLD  7915  rankbnd2  8068  domtri2  8151  infxpenc2  8180  infxpenc2OLD  8184  fseqdom  8188  acni2  8208  dfac9  8297  cfeq0  8417  cfsuc  8418  cflim3  8423  cfslb  8427  cofsmo  8430  enfin2i  8482  isfin3ds  8490  isf33lem  8527  fin1a2lem5  8565  axdc2lem  8609  zorn2g  8664  fodomb  8685  brdom7disj  8690  brdom6disj  8691  iundom2g  8696  cfpwsdom  8740  elgch  8781  fpwwe2cbv  8789  fpwwecbv  8803  pwfseqlem3  8819  pwfseqlem4a  8820  pwfseqlem4  8821  ltpiord  9048  nlt1pi  9067  nqereu  9090  addclprlem1  9177  1idpr  9190  reclem3pr  9210  ltsosr  9253  map2psrpr  9269  supsrlem  9270  axrrecex  9322  xrlenlt  9434  eqlei2  9477  addsubeq4  9617  renegcli  9662  lesub0  9848  wloglei  9864  conjmul  10040  rereccl  10041  infm3  10281  supmul1  10287  supmullem1  10288  supmullem2  10289  supmul  10290  creui  10309  nndiv  10354  elznn0  10653  prime  10714  eqreznegel  10932  zsupss  10936  rebtwnz  10944  ltxr  11087  elixx3g  11305  ixxun  11308  ioo0  11317  ico0  11338  ioc0  11339  icc0  11340  difreicc  11409  divelunit  11419  iccf1o  11421  elfz2  11436  fzn  11458  fznn  11518  fzshftral  11539  fzosplitsni  11626  om2uzisoi  11769  sq11i  11948  hashsdom  12136  euhash1  12164  brfi1uzind  12211  wrdval  12230  csbwrdg  12249  wrd2ind  12364  s2f1o  12518  cjreb  12604  rexfiuz  12827  cau3lem  12834  rlim2  12966  ello12  12986  ello1mpt  12991  elo12  12997  o1lo1  13007  lo1resb  13034  o1resb  13036  o1compt  13057  caucvgb  13149  mertens  13338  ruclem12  13515  divides  13529  odd2np1  13584  oddm1even  13585  sadadd2lem2  13638  gcdcllem2  13688  bezoutlem2  13715  bezoutlem3  13716  bezoutlem4  13717  isprm2  13763  isprm3  13764  prmreclem2  13970  prmreclem5  13973  prmreclem6  13974  4sqlem2  14002  4sqlem12  14009  vdwmc  14031  vdwpc  14033  vdwlem6  14039  vdwlem10  14043  vdwnn  14051  ramval  14061  0ram  14073  prdsleval  14407  pwsle  14422  imasleval  14471  xpsfrnel2  14495  xpsle  14511  isacs2  14583  mreacs  14588  acsfn  14589  iscatd2  14611  catpropd  14640  isssc  14725  evlfcl  15024  uncfcurf  15041  pltval  15122  lublecllem  15150  tosso  15198  oduleg  15294  oduclatb  15306  posglbmo  15309  isipodrs  15323  odudlatb  15358  gsumvalx  15493  grplmulf1o  15591  grplactcnv  15615  elnmz  15711  eqgid  15724  isghm  15738  ghmeqker  15764  resscntz  15840  symg1bas  15892  pgrpsubgsymgbi  15903  symgfixelq  15929  f1omvdconj  15943  odmulgeq  16049  sylow3lem3  16119  sylow3lem6  16122  efgval2  16212  efgsdm  16218  efgrelexlema  16237  efgcpbllemb  16243  iscyggen2  16349  cyggenod  16352  gsummptfzcl  16448  eldprd  16474  eldprdOLD  16476  dprdf11  16501  dprdf11OLD  16508  dprddisj2  16525  dprddisj2OLD  16526  pgpfac1lem2  16564  pgpfac1  16569  drngid2  16826  issubrg  16843  islmod  16930  aspval2  17394  psrbag  17408  zndvds  17957  znleval  17962  iunocv  18081  pjfval2  18109  pjdm2  18111  dsmmelbas  18139  ellspd  18205  ellspdOLD  18206  islindf  18216  islindf4  18242  istopg  18483  istpsOLD  18500  basgen2  18569  isclo  18666  mretopd  18671  isnei  18682  isperf3  18732  restdis  18757  neitr  18759  restcls  18760  restlp  18762  restperf  18763  iscn  18814  iscnp  18816  lmbr2  18838  lmbrf  18839  ordtt1  18958  cmpsub  18978  hauscmplem  18984  cmpfi  18986  bwthOLD  18989  dfcon2  18998  1stcelcls  19040  1stccn  19042  nllyi  19054  subislly  19060  elkgen  19084  ptpjpre1  19119  ptuni2  19124  ptclsg  19163  ptcnplem  19169  txcn  19174  hausdiag  19193  txhaus  19195  txkgen  19200  xkoptsub  19202  cnmpt21  19219  elqtop  19245  tgqtop  19260  r0cld  19286  elfg  19419  fbasrn  19432  trfil2  19435  trfil3  19436  fin1aufil  19480  elfm2  19496  elfm3  19498  flimopn  19523  fbflim  19524  flfnei  19539  flftg  19544  cnpflf2  19548  txflf  19554  fclsbas  19569  alexsubALTlem4  19597  cnextfvval  19612  snclseqg  19661  tgphaus  19662  tsmsfbas  19673  tsmssubm  19691  utopsnneip  19798  prdsxmetlem  19918  imasdsf1olem  19923  xpsdsval  19931  blres  19981  isxms2  19998  metcnp  20091  txmetcnp  20097  txmetcn  20098  metustelOLD  20101  metustel  20102  metuel2  20129  dscopn  20141  isngp4  20178  cnblcld  20329  metnrmlem1a  20409  icoopnst  20486  iocopnst  20487  elpi1  20592  lmmbr2  20745  cfil3i  20755  caucfil  20769  iscmet3  20779  lmclim  20788  metcld2  20792  bcthlem4  20813  minveclem3b  20890  minveclem6  20896  minveclem7  20897  ivthle  20915  ivthle2  20916  evthicc2  20919  ovolfioo  20926  ovolficc  20927  ovolgelb  20938  dyadmax  21053  subopnmbl  21059  ismbf3d  21107  mbfimaopnlem  21108  mbfimaopn2  21110  mbfaddlem  21113  mbfsup  21117  mbfinf  21118  i1f1lem  21142  i1fmulclem  21155  itg1climres  21167  mbfi1fseqlem4  21171  itg2monolem1  21203  itg2gt0  21213  isibl  21218  iblcnlem1  21240  ellimc2  21327  dvcnvrelem1  21464  itgsubst  21496  mdegleb  21510  fta1glem2  21613  quotval  21733  vieta1lem1  21751  vieta1lem2  21752  ulm2  21825  ulmcaulem  21834  ulmcau  21835  radcnvlt1  21858  sineq0  21958  cos11  21964  recosf1o  21966  efopn  22078  cxpeq  22170  mcubic  22217  birthdaylem3  22322  rlimcnp  22334  xrlimcnp  22337  wilth  22384  isppw  22427  isppw2  22428  mumullem2  22493  sqff1o  22495  dvdsmulf1o  22509  fsumvma  22527  fsumvma2  22528  vmasum  22530  chpchtsum  22533  lgsne0  22647  lgseisenlem2  22664  lgsquadlem1  22668  lgsquadlem2  22669  dchrmusumlema  22717  rpvmasum2  22736  dchrisum0lema  22738  pntibndlem3  22816  pntlemi  22828  pntleml  22835  pnt3  22836  trgcgrg  22942  colcom  22966  colrot1  22967  lncom  23000  mirreu3  23026  brbtwn  23096  brcgr  23097  brbtwn2  23102  colinearalg  23107  axeuclidlem  23159  axcontlem2  23162  axcontlem4  23164  axcontlem7  23167  nbgraf1olem1  23301  nbgraf1olem5  23305  nbcusgra  23322  uvtx01vtx  23351  cusgrauvtxb  23355  iswlk  23377  istrl  23387  ispth  23418  isspth  23419  wlkdvspthlem  23457  usgrcyclnl2  23478  eupath2  23552  grpodiveq  23694  opidon  23760  issmgrp  23772  ismndo  23781  isrngo  23816  isdivrngo  23869  isvclem  23906  isnvlem  23939  isphg  24168  isph  24173  phoeqi  24209  ubthlem3  24224  minvecolem5  24233  minvecolem6  24234  minvecolem7  24235  hhph  24531  issh3  24573  nmopub  25263  nmfnleub  25280  adjeq  25290  adjvalval  25292  elunop2  25368  lnophm  25374  nmcexi  25381  cnlnadjlem5  25426  cnlnadjeui  25432  adjbd1o  25440  jpi  25625  mddmd2  25664  chrelati  25719  chrelat2i  25720  cvexchlem  25723  dmdbr5ati  25777  cdjreui  25787  cdj3i  25796  preqsnd  25852  disjunsn  25887  opabdm  25894  opabrn  25895  abfmpunirn  25918  feqmptdf  25929  fmptcof2  25930  ofpreima  25935  funcnvmptOLD  25937  funcnvmpt  25938  funcnv5mpt  25939  f1od2  25975  resf1o  25981  fpwrelmap  25984  negelrp  25988  iocinioc2  26020  eliccioo  26057  posrasymb  26069  isslmd  26169  pstmxmet  26276  prsdm  26296  prsrn  26297  ordtconlem1  26306  xrmulc1cn  26312  eulerpartlemmf  26710  isrrvv  26778  eldmgm  26960  dmgmaddn0  26961  lgamgulmlem6  26972  subfacp1lem3  27022  subfacp1lem6  27025  subfacp1  27026  txpcon  27073  sconpi1  27080  rescon  27087  cvmscbv  27099  cvmsval  27107  cvmlift2lem13  27156  cvmlift3lem2  27161  cvmlift3  27169  br8  27517  br6  27518  br4  27519  distel  27568  elpred  27589  poseq  27665  wsuclem  27713  sltsolem1  27760  imageval  27912  funpartfv  27927  dfrdg4  27932  altopthg  27949  altopthbg  27950  brcolinear2  28040  lineext  28058  brsegle  28090  seglelin  28098  broutsideof2  28104  onsuct0  28239  wl-sbrimt  28325  wl-sblimt  28326  wl-sbnf1  28330  wl-mo2dnae  28348  wl-mo2t  28349  wl-mo3t  28350  wl-ax11-lem6  28359  supaddc  28370  supadd  28371  tan2h  28377  ptrest  28378  mbfposadd  28392  cnambfre  28393  itg2addnclem2  28397  isfne4  28494  isfne2  28496  isfne3  28497  fneval  28512  topfneec  28516  neibastop2lem  28534  neibastop2  28535  neifg  28545  filnetlem4  28555  fdc  28594  heibor1  28662  rrncmslem  28684  rrnheibor  28689  isfldidl2  28822  isdmn3  28827  prtlem13  28966  prter3  28980  ellz1  29058  lzunuz  29059  fz1eqin  29060  diophrex  29067  rexrabdioph  29085  rexfrabdioph  29086  2rexfrabdioph  29087  3rexfrabdioph  29088  4rexfrabdioph  29089  6rexfrabdioph  29090  7rexfrabdioph  29091  fzneg  29278  expdioph  29325  wepwsolem  29347  fnwe2lem2  29357  islmodfg  29375  kercvrlsm  29389  sdrgacs  29511  pm10.52  29570  iotasbc  29626  pm14.122a  29629  pm14.122b  29630  pm14.123a  29632  rusbcALT  29646  fvsb  29661  stoweidlem34  29782  2reu4a  29966  funressnfv  29987  dfafn5a  30019  el2xptp0  30080  otthg  30083  f12dfv  30099  f13dfv  30100  elfz2z  30151  usgra2pthlem1  30253  wwlkn0s  30292  wwlkextwrd  30313  usg2spthonot  30360  isclwlk0  30372  clwwlkn2  30391  eclclwwlkn1  30459  eleclclwwlkn  30460  hashecclwwlkn1  30461  usghashecclwwlk  30462  clwlkfclwwlk1hashn  30467  clwlkfoclwwlk  30471  isrgra  30496  isrusgra  30497  wwlkextproplem3  30515  frgra3vlem2  30546  frgrancvvdeqlem2  30577  frgrancvvdeqlem3  30578  frgrancvvdeqlemC  30585  usg2spot2nb  30611  opeliun2xp  30672  fmptsnd  30674  rabssnn0fi  30698  snlindsntor  30894  gte-lte  30948  gt-lt  30949  trsbc  31134  bnj976  31658  bnj944  31818  bnj1173  31880  bnj1321  31905  bnj1373  31908  bnj1417  31919  bj-iftru  31974  bj-iffal  31975  bj-abbi  32153  bj-tagcg  32325  bj-projval  32336  lrelat  32499  islshpat  32502  lshpsmreu  32594  lkrpssN  32648  cmtvalN  32696  omllaw2N  32729  cvrval  32754  cvrval2  32759  cvlsupr3  32829  3dim0  32941  islln2  32995  islpln5  33019  islpln2  33020  islpln2ah  33033  islvol5  33063  islvol2  33064  4atlem11  33093  pmapglbx  33253  cdleme18d  33779  cdlemefrs29bpre0  33880  cdlemb3  34090  cdlemg33b  34191  cdlemkid3N  34417  cdlemkid4  34418  dvhb1dimN  34470  dia11N  34533  cdlemm10N  34603  dib11N  34645  dib1dim  34650  dibglbN  34651  diblsmopel  34656  dihopelvalcpre  34733  dih11  34750  dihmeetlem4preN  34791  dihmeetlem13N  34804  lcfrvalsnN  35026  lcfrlem9  35035  lcf1o  35036  mapdval4N  35117  baerlem3lem2  35195  baerlem5alem2  35196  baerlem5blem2  35197  hdmap1fval  35282  hdmapfval  35315  hdmapglem7a  35415  hlhillcs  35446