Theorem syl5bb 257

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-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  1455  had1  1457  ax12wdemo  1817  sbal2  2191  abbiOLD  2575  necon3abid  2689  necon1abidOLD  2692  necon3bid  2701  r19.21tOLD  2841  ceqsralt  3119  ralxpxfr2d  3210  ceqsrexv  3219  ceqsrex2v  3221  elab2g  3234  elrabf  3241  elrab3t  3242  eueq2  3259  eqreu  3277  reu8  3281  ru  3312  sbcralt  3394  sbcabel  3402  sbcel1g  3815  sbcel2  3817  csbnestgf  3826  sbccsb2  3837  disjpss  3863  sbcssg  3925  rexsng  4050  ralprg  4063  rexprg  4064  difsn  4149  opthpr  4193  ralunsn  4222  csbuni  4262  dfiin2g  4348  iunxsng  4394  elpwuni  4403  disjxun  4435  sbcbr12g  4491  pwnss  4602  opthneg  4716  otthg  4720  opelopabt  4749  opelopabga  4750  brabga  4751  csbmpt12  4771  dfid3  4786  frirr  4846  wereu2  4866  ordtri4  4905  oneqmini  4919  elsucg  4935  elsuc2g  4936  brab2a  5039  opeliunxp  5041  posn  5058  sosn  5059  frsn  5060  brab2ga  5065  opbrop  5069  csbcnvgALT  5177  elrnmpt1  5241  elrnmptg  5242  eliniseg2  5366  poleloe  5391  xpdifid  5425  cnvpo  5535  sbcfung  5601  dffun8  5605  fncnv  5642  fununi  5644  fnssresb  5683  fnimaeq0  5692  funcocnv2  5830  csbfv12  5891  dffn5  5903  funimass4  5909  fnsnfv  5918  dmfco  5932  fndmdif  5976  fvimacnvi  5986  fvimacnvALT  5991  unpreima  5998  respreima  6001  fmptco  6049  fressnfv  6070  fmptsnd  6078  fnnfpeq0  6087  fnsuppresOLD  6116  elunirn  6148  dff13  6151  f12dfv  6164  f13dfv  6165  fliftel  6192  isoini  6219  f1oiso  6232  eloprabga  6374  resoprab2  6384  elrnmpt2res  6401  ralrnmpt2  6402  ovid  6404  ov  6407  ovg  6426  ofrfval2  6542  dfwe2  6602  ssonprc  6612  ordpwsuc  6635  dfom2  6687  f1oweALT  6769  el2xptp0  6829  fmpt2x  6851  ovmptss  6866  1stconst  6873  2ndconst  6874  fnsuppres  6929  isprmpt2  6955  brtpos2  6963  mpt2curryd  7000  dfsmo2  7020  rdglim2  7100  seqomlem2  7118  omeu  7236  oeeui  7253  brdifun  7340  eqerlem  7345  brecop  7406  erovlem  7409  eceqoveq  7418  mapsn  7462  ixpsnval  7474  mptelixpg  7508  map1  7596  xpsnen  7603  xpdom2  7614  omxpenlem  7620  xpf1o  7681  mapunen  7688  onfin  7710  fimaxg  7769  fodomfib  7802  fofinf1o  7803  fipreima  7828  supub  7921  ordtypecbv  7945  ordtypelem3  7948  ordtypelem9  7954  hartogslem1  7970  wofib  7973  wemapsolem  7978  wemapso2OLD  7980  wemapso2lem  7981  noinfep  8079  noinfepOLD  8080  cantnf  8115  cantnfOLD  8137  rankbnd2  8290  domtri2  8373  infxpenc2  8402  infxpenc2OLD  8406  fseqdom  8410  acni2  8430  dfac9  8519  cfeq0  8639  cfsuc  8640  cflim3  8645  cfslb  8649  cofsmo  8652  enfin2i  8704  isfin3ds  8712  isf33lem  8749  fin1a2lem5  8787  axdc2lem  8831  zorn2g  8886  fodomb  8907  brdom7disj  8912  brdom6disj  8913  iundom2g  8918  cfpwsdom  8962  elgch  9003  fpwwe2cbv  9011  fpwwecbv  9025  pwfseqlem3  9041  pwfseqlem4a  9042  pwfseqlem4  9043  ltpiord  9268  nlt1pi  9287  nqereu  9310  addclprlem1  9397  1idpr  9410  reclem3pr  9430  ltsosr  9474  map2psrpr  9490  supsrlem  9491  axrrecex  9543  xrlenlt  9655  eqlei2  9698  addsubeq4  9840  renegcli  9885  lesub0  10076  wloglei  10092  conjmul  10268  rereccl  10269  infm3  10509  supmul1  10515  supmullem1  10516  supmullem2  10517  supmul  10518  creui  10538  nndiv  10583  elznn0  10886  prime  10950  eqreznegel  11178  zsupss  11182  rebtwnz  11192  ltxr  11335  elixx3g  11553  ixxun  11556  ioo0  11565  ico0  11586  ioc0  11587  icc0  11588  difreicc  11663  divelunit  11673  iccf1o  11675  elfz2  11690  fzn  11713  fznn  11758  fzshftral  11777  fzosplitsni  11902  om2uzisoi  12047  rabssnn0fi  12077  mptnn0fsupp  12085  sq11i  12240  hashsdom  12431  brfi1uzind  12514  wrdval  12533  csbwrdg  12552  wrd2ind  12685  s2f1o  12846  cjreb  12938  rexfiuz  13162  cau3lem  13169  rlim2  13301  ello12  13321  ello1mpt  13326  elo12  13332  o1lo1  13342  lo1resb  13369  o1resb  13371  o1compt  13392  caucvgb  13484  mertens  13677  ruclem12  13956  divides  13970  odd2np1  14028  oddm1even  14029  sadadd2lem2  14082  gcdcllem2  14132  bezoutlem2  14159  bezoutlem3  14160  bezoutlem4  14161  isprm2  14207  isprm3  14208  prmreclem2  14417  prmreclem5  14420  prmreclem6  14421  4sqlem2  14449  4sqlem12  14456  vdwmc  14478  vdwpc  14480  vdwlem6  14486  vdwlem10  14490  vdwnn  14498  ramval  14508  0ram  14520  prdsleval  14856  pwsle  14871  imasleval  14920  xpsfrnel2  14944  xpsle  14960  isacs2  15032  mreacs  15037  acsfn  15038  iscatd2  15060  catpropd  15086  isssc  15171  evlfcl  15470  uncfcurf  15487  pltval  15569  lublecllem  15597  tosso  15645  oduleg  15741  oduclatb  15753  posglbmo  15756  isipodrs  15770  odudlatb  15805  gsumvalx  15876  sgrp2rid2  16023  grplmulf1o  16091  grplactcnv  16117  elnmz  16219  eqgid  16232  isghm  16246  ghmeqker  16272  resscntz  16348  symg1bas  16400  pgrpsubgsymgbi  16411  symgfixelq  16437  f1omvdconj  16450  odmulgeq  16558  sylow3lem3  16628  sylow3lem6  16631  efgval2  16721  efgsdm  16727  efgrelexlema  16746  efgcpbllemb  16752  iscyggen2  16863  cyggenod  16866  gsummptfzcl  16975  eldprd  17014  eldprdOLD  17016  dprdf11  17042  dprdf11OLD  17049  dprddisj2  17066  dprddisj2OLD  17067  pgpfac1lem2  17105  pgpfac1  17110  srg1zr  17159  drngid2  17391  issubrg  17408  islmod  17495  aspval2  17975  psrbag  17992  cply1coe0bi  18321  zndvds  18566  znleval  18571  iunocv  18690  pjfval2  18718  pjdm2  18720  dsmmelbas  18748  ellspd  18814  ellspdOLD  18815  islindf  18825  islindf4  18851  istopg  19382  istpsOLD  19399  basgen2  19469  isclo  19566  mretopd  19571  isnei  19582  isperf3  19632  restdis  19657  neitr  19659  restcls  19660  restlp  19662  restperf  19663  iscn  19714  iscnp  19716  lmbr2  19738  lmbrf  19739  ordtt1  19858  cmpsub  19878  hauscmplem  19884  cmpfi  19886  bwthOLD  19889  dfcon2  19898  1stcelcls  19940  1stccn  19942  nllyi  19954  subislly  19960  dissnlocfin  20008  elkgen  20015  ptpjpre1  20050  ptuni2  20055  ptclsg  20094  ptcnplem  20100  txcn  20105  hausdiag  20124  txhaus  20126  txkgen  20131  xkoptsub  20133  cnmpt21  20150  elqtop  20176  tgqtop  20191  r0cld  20217  elfg  20350  fbasrn  20363  trfil2  20366  trfil3  20367  fin1aufil  20411  elfm2  20427  elfm3  20429  flimopn  20454  fbflim  20455  flfnei  20470  flftg  20475  cnpflf2  20479  txflf  20485  fclsbas  20500  alexsubALTlem4  20528  cnextfvval  20543  snclseqg  20592  tgphaus  20593  tsmsfbas  20604  tsmssubm  20622  utopsnneip  20729  prdsxmetlem  20849  imasdsf1olem  20854  xpsdsval  20862  blres  20912  isxms2  20929  metcnp  21022  txmetcnp  21028  txmetcn  21029  metustelOLD  21032  metustel  21033  metuel2  21060  dscopn  21072  isngp4  21109  cnblcld  21260  metnrmlem1a  21340  icoopnst  21417  iocopnst  21418  elpi1  21523  lmmbr2  21676  cfil3i  21686  caucfil  21700  iscmet3  21710  lmclim  21719  metcld2  21723  bcthlem4  21744  minveclem3b  21821  minveclem6  21827  minveclem7  21828  ivthle  21846  ivthle2  21847  evthicc2  21850  ovolfioo  21857  ovolficc  21858  ovolgelb  21869  dyadmax  21985  subopnmbl  21991  ismbf3d  22039  mbfimaopnlem  22040  mbfimaopn2  22042  mbfaddlem  22045  mbfsup  22049  mbfinf  22050  i1f1lem  22074  i1fmulclem  22087  itg1climres  22099  mbfi1fseqlem4  22103  itg2monolem1  22135  itg2gt0  22145  isibl  22150  iblcnlem1  22172  ellimc2  22259  dvcnvrelem1  22396  itgsubst  22428  mdegleb  22442  fta1glem2  22545  quotval  22666  vieta1lem1  22684  vieta1lem2  22685  ulm2  22758  ulmcaulem  22767  ulmcau  22768  radcnvlt1  22791  sineq0  22892  cos11  22898  recosf1o  22900  efopn  23017  cxpeq  23109  mcubic  23156  birthdaylem3  23261  rlimcnp  23273  xrlimcnp  23276  wilth  23323  isppw  23366  isppw2  23367  mumullem2  23432  sqff1o  23434  dvdsmulf1o  23448  fsumvma  23466  fsumvma2  23467  vmasum  23469  chpchtsum  23472  lgsne0  23586  lgseisenlem2  23603  lgsquadlem1  23607  lgsquadlem2  23608  dchrmusumlema  23656  rpvmasum2  23675  dchrisum0lema  23677  pntibndlem3  23755  pntlemi  23767  pntleml  23774  pnt3  23775  trgcgrg  23884  colcom  23923  colrot1  23924  ltgov  23961  hlcomb  23965  lncom  23980  mirreu3  24013  isperp  24067  perpcom  24068  brbtwn  24180  brcgr  24181  brbtwn2  24186  colinearalg  24191  axeuclidlem  24243  axcontlem2  24246  axcontlem4  24248  axcontlem7  24251  nbgraf1olem1  24419  nbgraf1olem5  24423  nbcusgra  24441  uvtx01vtx  24470  cusgrauvtxb  24474  iswlk  24498  istrl  24517  ispth  24548  isspth  24549  wlkdvspthlem  24587  usgrcyclnl2  24619  wwlkn0s  24683  wwlkextwrd  24706  wwlkextproplem3  24721  isclwlk0  24732  clwwlkn2  24753  eclclwwlkn1  24810  eleclclwwlkn  24811  hashecclwwlkn1  24812  usghashecclwwlk  24813  clwlkfclwwlk1hashn  24819  clwlkfoclwwlk  24823  usg2spthonot  24866  isrgra  24904  isrusgra  24905  isrusgusrg  24910  eupath2  24958  frgra3vlem2  24979  frgrancvvdeqlem2  25009  frgrancvvdeqlem3  25010  frgrancvvdeqlemC  25017  usg2spot2nb  25043  grpodiveq  25236  opidonOLD  25302  issmgrpOLD  25314  ismndo  25323  isrngo  25358  isdivrngo  25411  isvclem  25448  isnvlem  25481  isphg  25710  isph  25715  phoeqi  25751  ubthlem3  25766  minvecolem5  25775  minvecolem6  25776  minvecolem7  25777  hhph  26073  issh3  26115  nmopub  26805  nmfnleub  26822  adjeq  26832  adjvalval  26834  elunop2  26910  lnophm  26916  nmcexi  26923  cnlnadjlem5  26968  cnlnadjeui  26974  adjbd1o  26982  jpi  27167  mddmd2  27206  chrelati  27261  chrelat2i  27262  cvexchlem  27265  dmdbr5ati  27319  cdjreui  27329  cdj3i  27338  preqsnd  27396  disjunsn  27431  opeldifid  27434  fcoinvbr  27439  opabdm  27442  opabrn  27443  abfmpunirn  27468  feqmptdf  27479  fmptcof2  27480  funcnvmptOLD  27487  funcnvmpt  27488  funcnv5mpt  27489  f1od2  27525  resf1o  27531  fpwrelmap  27534  negelrp  27542  iocinioc2  27568  eliccioo  27605  posrasymb  27623  isslmd  27723  pstmxmet  27854  prsdm  27874  prsrn  27875  ordtconlem1  27884  xrmulc1cn  27890  eulerpartlemmf  28292  isrrvv  28360  eldmgm  28542  dmgmaddn0  28543  lgamgulmlem6  28554  subfacp1lem3  28604  subfacp1lem6  28607  subfacp1  28608  txpcon  28655  sconpi1  28662  rescon  28669  cvmscbv  28681  cvmsval  28689  cvmlift2lem13  28738  cvmlift3lem2  28743  cvmlift3  28751  mclsrcl  28899  br8  29161  br6  29162  br4  29163  distel  29212  elpred  29233  poseq  29309  wsuclem  29357  sltsolem1  29404  imageval  29556  funpartfv  29571  dfrdg4  29576  altopthg  29593  altopthbg  29594  brcolinear2  29684  lineext  29702  brsegle  29734  seglelin  29742  broutsideof2  29748  onsuct0  29882  wl-sbrimt  29974  wl-sblimt  29975  wl-sbnf1  29979  wl-mo2dnae  29995  wl-mo2t  29996  wl-mo3t  29997  wl-ax11-lem6  30006  supaddc  30017  supadd  30018  tan2h  30023  ptrest  30024  mbfposadd  30038  cnambfre  30039  itg2addnclem2  30043  isfne4  30134  isfne2  30136  isfne3  30137  fneval  30146  topfneec  30149  neibastop2lem  30154  neibastop2  30155  neifg  30165  filnetlem4  30175  fdc  30214  heibor1  30282  rrncmslem  30304  rrnheibor  30309  isfldidl2  30442  isdmn3  30447  prtlem13  30585  prter3  30599  ellz1  30676  lzunuz  30677  fz1eqin  30678  diophrex  30685  rexrabdioph  30703  rexfrabdioph  30704  2rexfrabdioph  30705  3rexfrabdioph  30706  4rexfrabdioph  30707  6rexfrabdioph  30708  7rexfrabdioph  30709  fzneg  30896  expdioph  30941  wepwsolem  30963  fnwe2lem2  30973  islmodfg  30991  kercvrlsm  31005  sdrgacs  31126  pm10.52  31224  iotasbc  31280  pm14.122a  31283  pm14.122b  31284  pm14.123a  31286  rusbcALT  31300  fvsb  31315  limcperiod  31588  limsupre  31601  dvbdfbdioo  31681  stoweidlem34  31770  fourierdlem108  31951  fourierdlem110  31953  2reu4a  32148  funressnfv  32167  dfafn5a  32199  elfz2z  32285  usgra2pthlem1  32307  isuhgr  32320  isushgr  32321  usgo0s0ALT  32390  usgo1s0ALT  32391  tpres  32506  inclfusubc  32517  isrnghm  32533  rnghmval2  32536  uzlidlring  32562  lidldomnnring  32563  opeliun2xp  32790  snlindsntor  32942  gte-lte  32988  gt-lt  32989  trsbc  33179  bnj976  33704  bnj944  33864  bnj1173  33926  bnj1321  33951  bnj1373  33954  bnj1417  33965  bj-iftru  34035  bj-iffal  34036  bj-abbi  34244  bj-tagcg  34426  bj-projval  34437  lrelat  34614  islshpat  34617  lshpsmreu  34709  lkrpssN  34763  cmtvalN  34811  omllaw2N  34844  cvrval  34869  cvrval2  34874  cvlsupr3  34944  3dim0  35056  islln2  35110  islpln5  35134  islpln2  35135  islpln2ah  35148  islvol5  35178  islvol2  35179  4atlem11  35208  pmapglbx  35368  cdleme18d  35895  cdlemefrs29bpre0  35997  cdlemb3  36207  cdlemg33b  36308  cdlemkid3N  36534  cdlemkid4  36535  dvhb1dimN  36587  dia11N  36650  cdlemm10N  36720  dib11N  36762  dib1dim  36767  dibglbN  36768  diblsmopel  36773  dihopelvalcpre  36850  dih11  36867  dihmeetlem4preN  36908  dihmeetlem13N  36921  lcfrvalsnN  37143  lcfrlem9  37152  lcf1o  37153  mapdval4N  37234  baerlem3lem2  37312  baerlem5alem2  37313  baerlem5blem2  37314  hdmap1fval  37399  hdmapfval  37432  hdmapglem7a  37532  hlhillcs  37563