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  365  ifptruOLD  1392  ifpfal  1393  ifpfalOLD  1394  cad0  1475  had1  1478  ax12wdemo  1839  sbal2  2209  abbiOLD  2514  necon3abid  2628  necon1abidOLD  2631  necon3bid  2640  r19.21tOLD  2780  ceqsralt  3058  ralxpxfr2d  3149  ceqsrexv  3158  ceqsrex2v  3160  elab2g  3173  elrabf  3180  elrab3t  3181  eueq2  3198  eqreu  3216  reu8  3220  ru  3251  sbcralt  3325  sbcabel  3330  sbcel1g  3754  sbcel2  3756  csbnestgf  3763  sbccsb2  3772  disjpss  3793  sbcssg  3856  rexsng  3980  ralprg  3993  rexprg  3994  difsn  4078  opthpr  4122  ralunsn  4151  csbuni  4191  dfiin2g  4276  iunxsng  4325  elpwuni  4334  disjxun  4365  sbcbr12g  4420  pwnss  4530  opthneg  4641  otthg  4645  opelopabt  4673  opelopabga  4674  brabga  4675  csbmpt12  4695  dfid3  4710  frirr  4770  wereu2  4790  ordtri4  4829  oneqmini  4843  elsucg  4859  elsuc2g  4860  brab2a  4963  opeliunxp  4965  posn  4982  sosn  4983  frsn  4984  brab2ga  4989  opbrop  4993  csbcnvgALT  5100  elrnmpt1  5164  elrnmptg  5165  eliniseg2  5289  poleloe  5311  xpdifid  5345  cnvpo  5454  sbcfung  5519  dffun8  5523  fncnv  5560  fununi  5562  fnssresb  5601  fnimaeq0  5610  funcocnv2  5748  csbfv12  5809  dffn5  5819  funimass4  5825  fnsnfv  5834  dmfco  5848  fndmdif  5893  fvimacnvi  5903  fvimacnvALT  5908  unpreima  5915  respreima  5918  fmptco  5966  fressnfv  5987  fmptsnd  5995  fnnfpeq0  6004  tpres  6026  fnsuppresOLD  6033  elunirn  6064  dff13  6067  f12dfv  6080  f13dfv  6081  fliftel  6108  isoini  6135  f1oiso  6148  eloprabga  6288  resoprab2  6298  elrnmpt2res  6315  ralrnmpt2  6316  ovid  6318  ov  6321  ovg  6340  ofrfval2  6456  dfwe2  6516  ssonprc  6526  ordpwsuc  6549  dfom2  6601  f1oweALT  6683  el2xptp0  6743  fmpt2x  6765  ovmptss  6780  1stconst  6787  2ndconst  6788  fnsuppres  6845  isprmpt2  6871  brtpos2  6879  mpt2curryd  6916  dfsmo2  6936  rdglim2  7016  seqomlem2  7034  omeu  7152  oeeui  7169  brdifun  7256  eqerlem  7261  brecop  7322  erovlem  7325  eceqoveq  7334  mapsn  7379  ixpsnval  7391  mptelixpg  7425  map1  7513  xpsnen  7520  xpdom2  7531  omxpenlem  7537  xpf1o  7598  mapunen  7605  onfin  7627  fimaxg  7682  fodomfib  7715  fofinf1o  7716  fipreima  7741  supub  7833  ordtypecbv  7857  ordtypelem3  7860  ordtypelem9  7866  hartogslem1  7882  wofib  7885  wemapsolem  7890  wemapso2OLD  7892  wemapso2lem  7893  noinfep  7990  cantnf  8025  cantnfOLD  8047  rankbnd2  8200  domtri2  8283  infxpenc2  8312  infxpenc2OLD  8316  fseqdom  8320  acni2  8340  dfac9  8429  cfeq0  8549  cfsuc  8550  cflim3  8555  cfslb  8559  cofsmo  8562  enfin2i  8614  isfin3ds  8622  isf33lem  8659  fin1a2lem5  8697  axdc2lem  8741  zorn2g  8796  fodomb  8817  brdom7disj  8822  brdom6disj  8823  iundom2g  8828  cfpwsdom  8872  elgch  8911  fpwwe2cbv  8919  fpwwecbv  8933  pwfseqlem3  8949  pwfseqlem4a  8950  pwfseqlem4  8951  ltpiord  9176  nlt1pi  9195  nqereu  9218  addclprlem1  9305  1idpr  9318  reclem3pr  9338  ltsosr  9382  map2psrpr  9398  supsrlem  9399  axrrecex  9451  xrlenlt  9563  eqlei2  9606  addsubeq4  9748  renegcli  9793  lesub0  9987  wloglei  10002  conjmul  10178  rereccl  10179  infm3  10418  supmul1  10424  supmullem1  10425  supmullem2  10426  supmul  10427  creui  10447  nndiv  10493  elznn0  10796  prime  10860  eqreznegel  11086  zsupss  11090  rebtwnz  11100  ltxr  11245  elixx3g  11463  ixxun  11466  ioo0  11475  ico0  11496  ioc0  11497  icc0  11498  difreicc  11573  divelunit  11583  iccf1o  11585  elfz2  11600  fzn  11623  fznn  11669  fzshftral  11688  nelfzo  11727  fzosplitsni  11819  om2uzisoi  11968  rabssnn0fi  11998  mptnn0fsupp  12006  sq11i  12161  hashsdom  12352  brfi1uzind  12436  wrdval  12456  csbwrdg  12478  wrd2ind  12614  s2f1o  12775  cjreb  12958  rexfiuz  13182  cau3lem  13189  rlim2  13321  ello12  13341  ello1mpt  13346  elo12  13352  o1lo1  13362  lo1resb  13389  o1resb  13391  o1compt  13412  caucvgb  13504  mertens  13697  ruclem12  13976  divides  13990  odd2np1  14048  oddm1even  14049  sadadd2lem2  14102  gcdcllem2  14152  bezoutlem2  14179  bezoutlem3  14180  bezoutlem4  14181  isprm2  14227  isprm3  14228  prmreclem2  14437  prmreclem5  14440  prmreclem6  14441  4sqlem2  14469  4sqlem12  14476  vdwmc  14498  vdwpc  14500  vdwlem6  14506  vdwlem10  14510  vdwnn  14518  ramval  14528  0ram  14540  prdsleval  14884  pwsle  14899  imasleval  14948  xpsfrnel2  14972  xpsle  14988  isacs2  15060  mreacs  15065  acsfn  15066  iscatd2  15088  catpropd  15115  ciclcl  15208  cicrcl  15209  isssc  15226  evlfcl  15608  uncfcurf  15625  pltval  15707  lublecllem  15735  tosso  15783  oduleg  15879  oduclatb  15891  posglbmo  15894  isipodrs  15908  odudlatb  15943  gsumvalx  16014  sgrp2rid2  16161  grplmulf1o  16229  grplactcnv  16255  elnmz  16357  eqgid  16370  isghm  16384  ghmeqker  16410  resscntz  16486  symg1bas  16538  pgrpsubgsymgbi  16549  symgfixelq  16575  f1omvdconj  16588  odmulgeq  16696  sylow3lem3  16766  sylow3lem6  16769  efgval2  16859  efgsdm  16865  efgrelexlema  16884  efgcpbllemb  16890  iscyggen2  17001  cyggenod  17004  gsummptfzcl  17110  eldprd  17148  eldprdOLD  17150  dprdf11  17176  dprdf11OLD  17183  dprddisj2  17200  dprddisj2OLD  17201  pgpfac1lem2  17239  pgpfac1  17244  srg1zr  17293  drngid2  17525  issubrg  17542  islmod  17629  aspval2  18109  psrbag  18126  cply1coe0bi  18455  zndvds  18679  znleval  18684  iunocv  18803  pjfval2  18831  pjdm2  18833  dsmmelbas  18861  ellspd  18922  islindf  18932  islindf4  18958  istopg  19489  istpsOLD  19506  basgen2  19576  isclo  19674  mretopd  19679  isnei  19690  isperf3  19740  restdis  19765  neitr  19767  restcls  19768  restlp  19770  restperf  19771  iscn  19822  iscnp  19824  lmbr2  19846  lmbrf  19847  ordtt1  19966  cmpsub  19986  hauscmplem  19992  cmpfi  19994  dfcon2  20005  1stcelcls  20047  1stccn  20049  nllyi  20061  subislly  20067  dissnlocfin  20115  elkgen  20122  ptpjpre1  20157  ptuni2  20162  ptclsg  20201  ptcnplem  20207  txcn  20212  hausdiag  20231  txhaus  20233  txkgen  20238  xkoptsub  20240  cnmpt21  20257  elqtop  20283  tgqtop  20298  r0cld  20324  elfg  20457  fbasrn  20470  trfil2  20473  trfil3  20474  fin1aufil  20518  elfm2  20534  elfm3  20536  flimopn  20561  fbflim  20562  flfnei  20577  flftg  20582  cnpflf2  20586  txflf  20592  fclsbas  20607  alexsubALTlem4  20635  cnextfvval  20650  snclseqg  20699  tgphaus  20700  tsmsfbas  20711  tsmssubm  20729  utopsnneip  20836  prdsxmetlem  20956  imasdsf1olem  20961  xpsdsval  20969  blres  21019  isxms2  21036  metcnp  21129  txmetcnp  21135  txmetcn  21136  metustelOLD  21139  metustel  21140  metuel2  21167  dscopn  21179  isngp4  21216  cnblcld  21367  metnrmlem1a  21447  icoopnst  21524  iocopnst  21525  elpi1  21630  lmmbr2  21783  cfil3i  21793  caucfil  21807  iscmet3  21817  lmclim  21826  metcld2  21830  bcthlem4  21851  minveclem3b  21928  minveclem6  21934  minveclem7  21935  ivthle  21953  ivthle2  21954  evthicc2  21957  ovolfioo  21964  ovolficc  21965  ovolgelb  21976  dyadmax  22092  subopnmbl  22098  ismbf3d  22146  mbfimaopnlem  22147  mbfimaopn2  22149  mbfaddlem  22152  mbfsup  22156  mbfinf  22157  i1f1lem  22181  i1fmulclem  22194  itg1climres  22206  mbfi1fseqlem4  22210  itg2monolem1  22242  itg2gt0  22252  isibl  22257  iblcnlem1  22279  ellimc2  22366  dvcnvrelem1  22503  itgsubst  22535  mdegleb  22549  fta1glem2  22652  quotval  22773  vieta1lem1  22791  vieta1lem2  22792  ulm2  22865  ulmcaulem  22874  ulmcau  22875  radcnvlt1  22898  sineq0  22999  cos11  23005  recosf1o  23007  efopn  23126  cxpeq  23218  mcubic  23294  birthdaylem3  23400  rlimcnp  23412  xrlimcnp  23415  wilth  23462  isppw  23505  isppw2  23506  mumullem2  23571  sqff1o  23573  dvdsmulf1o  23587  fsumvma  23605  fsumvma2  23606  vmasum  23608  chpchtsum  23611  lgsne0  23725  lgseisenlem2  23742  lgsquadlem1  23746  lgsquadlem2  23747  dchrmusumlema  23795  rpvmasum2  23814  dchrisum0lema  23816  pntibndlem3  23894  pntlemi  23906  pntleml  23913  pnt3  23914  trgcgrg  24026  colcom  24065  colrot1  24066  ltgov  24103  hlcomb  24107  lncom  24122  mirreu3  24155  isperp  24209  perpcom  24210  brbtwn  24323  brcgr  24324  brbtwn2  24329  colinearalg  24334  axeuclidlem  24386  axcontlem2  24389  axcontlem4  24391  axcontlem7  24394  nbgraf1olem1  24562  nbgraf1olem5  24566  nbcusgra  24584  uvtx01vtx  24613  cusgrauvtxb  24617  iswlk  24641  istrl  24660  ispth  24691  isspth  24692  wlkdvspthlem  24730  usgrcyclnl2  24762  wwlkn0s  24826  wwlkextwrd  24849  wwlkextproplem3  24864  isclwlk0  24875  clwwlkn2  24896  eclclwwlkn1  24953  eleclclwwlkn  24954  hashecclwwlkn1  24955  usghashecclwwlk  24956  clwlkfclwwlk1hashn  24962  clwlkfoclwwlk  24966  usg2spthonot  25009  isrgra  25047  isrusgra  25048  isrusgusrg  25053  eupath2  25101  frgra3vlem2  25122  frgrancvvdeqlem2  25152  frgrancvvdeqlem3  25153  frgrancvvdeqlemC  25160  usg2spot2nb  25186  grpodiveq  25375  opidonOLD  25441  issmgrpOLD  25453  ismndo  25462  isrngo  25497  isdivrngo  25550  isvclem  25587  isnvlem  25620  isphg  25849  isph  25854  phoeqi  25890  ubthlem3  25905  minvecolem5  25914  minvecolem6  25915  minvecolem7  25916  hhph  26212  issh3  26254  nmopub  26943  nmfnleub  26960  adjeq  26970  adjvalval  26972  elunop2  27048  lnophm  27054  nmcexi  27061  cnlnadjlem5  27106  cnlnadjeui  27112  adjbd1o  27120  jpi  27305  mddmd2  27344  chrelati  27399  chrelat2i  27400  cvexchlem  27403  dmdbr5ati  27457  cdjreui  27467  cdj3i  27476  preqsnd  27543  iunxsngf  27553  disjunsn  27583  opeldifid  27589  fcoinvbr  27594  brabgaf  27595  opabdm  27598  opabrn  27599  iunsnima  27604  abfmpunirn  27630  feqmptdf  27642  fmptcof2  27643  funcnvmptOLD  27655  funcnvmpt  27656  funcnv5mpt  27657  f1od2  27697  resf1o  27703  fpwrelmap  27706  negelrp  27714  iocinioc2  27743  eliccioo  27780  posrasymb  27798  isslmd  27898  pstmxmet  28030  prsdm  28050  prsrn  28051  ordtconlem1  28060  xrmulc1cn  28066  ispisys2  28302  elcarsg  28432  eulerpartlemmf  28497  isrrvv  28565  eldmgm  28753  dmgmaddn0  28754  lgamgulmlem6  28765  subfacp1lem3  28815  subfacp1lem6  28818  subfacp1  28819  txpcon  28866  sconpi1  28873  rescon  28880  cvmscbv  28892  cvmsval  28900  cvmlift2lem13  28949  cvmlift3lem2  28954  cvmlift3  28962  mclsrcl  29110  br8  29351  br6  29352  br4  29353  distel  29401  elpred  29422  poseq  29498  wsuclem  29546  sltsolem1  29593  imageval  29733  funpartfv  29748  dfrdg4  29753  altopthg  29770  altopthbg  29771  brcolinear2  29861  lineext  29879  brsegle  29911  seglelin  29919  broutsideof2  29925  onsuct0  30059  wl-sbrimt  30163  wl-sblimt  30164  wl-sbnf1  30168  wl-mo2dnae  30184  wl-mo2t  30185  wl-mo3t  30186  wl-ax11-lem6  30195  supaddc  30206  supadd  30207  tan2h  30212  ptrest  30213  mbfposadd  30227  cnambfre  30228  itg2addnclem2  30233  isfne4  30324  isfne2  30326  isfne3  30327  fneval  30336  topfneec  30339  neibastop2lem  30344  neibastop2  30345  neifg  30355  filnetlem4  30365  fdc  30404  heibor1  30472  rrncmslem  30494  rrnheibor  30499  isfldidl2  30632  isdmn3  30637  prtlem13  30775  prter3  30789  ellz1  30865  lzunuz  30866  fz1eqin  30867  diophrex  30874  rexrabdioph  30893  rexfrabdioph  30894  2rexfrabdioph  30895  3rexfrabdioph  30896  4rexfrabdioph  30897  6rexfrabdioph  30898  7rexfrabdioph  30899  fzneg  31085  expdioph  31131  wepwsolem  31153  fnwe2lem2  31163  islmodfg  31181  kercvrlsm  31195  sdrgacs  31318  pm10.52  31438  iotasbc  31494  pm14.122a  31497  pm14.122b  31498  pm14.123a  31500  rusbcALT  31514  fvsb  31529  limcperiod  31800  limsupre  31813  dvbdfbdioo  31893  stoweidlem34  31982  fourierdlem108  32163  fourierdlem110  32165  etransc  32232  2reu4a  32360  funressnfv  32379  dfafn5a  32411  dfeven2  32492  elfz2z  32652  usgra2pthlem1  32671  isuhgr  32684  isushgr  32685  usgo0s0ALT  32754  usgo1s0ALT  32755  ismhm0  32811  inclfusubc  32873  isrnghm  32898  rnghmval2  32901  uzlidlring  32935  lidldomnnring  32936  zrninitoringc  33079  opeliun2xp  33122  snlindsntor  33272  elbigo2  33373  gte-lte  33454  gt-lt  33455  trsbc  33647  bnj976  34183  bnj944  34343  bnj1173  34405  bnj1321  34430  bnj1373  34433  bnj1417  34444  bj-abbi  34708  bj-tagcg  34891  bj-projval  34902  lrelat  35152  islshpat  35155  lshpsmreu  35247  lkrpssN  35301  cmtvalN  35349  omllaw2N  35382  cvrval  35407  cvrval2  35412  cvlsupr3  35482  3dim0  35594  islln2  35648  islpln5  35672  islpln2  35673  islpln2ah  35686  islvol5  35716  islvol2  35717  4atlem11  35746  pmapglbx  35906  cdleme18d  36433  cdlemefrs29bpre0  36535  cdlemb3  36745  cdlemg33b  36846  cdlemkid3N  37072  cdlemkid4  37073  dvhb1dimN  37125  dia11N  37188  cdlemm10N  37258  dib11N  37300  dib1dim  37305  dibglbN  37306  diblsmopel  37311  dihopelvalcpre  37388  dih11  37405  dihmeetlem4preN  37446  dihmeetlem13N  37459  lcfrvalsnN  37681  lcfrlem9  37690  lcf1o  37691  mapdval4N  37772  baerlem3lem2  37850  baerlem5alem2  37851  baerlem5blem2  37852  hdmap1fval  37937  hdmapfval  37970  hdmapglem7a  38070  hlhillcs  38101  iunrelexpuztr  38224  brtrclfv2  38258