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  1452  had1  1454  ax12wdemo  1780  sbal2  2195  abbiOLD  2599  necon3abid  2713  necon1abidOLD  2716  necon3bid  2725  r19.21tOLD  2862  ceqsralt  3137  ralxpxfr2d  3228  ceqsrexv  3237  ceqsrex2v  3239  elab2g  3252  elrabf  3259  eueq2  3277  eqreu  3295  reu8  3299  ru  3330  sbcralt  3412  sbcabel  3420  sbcel1g  3829  sbcel2  3831  csbnestgf  3840  sbccsb2  3851  disjpss  3877  sbcssg  3938  rexsng  4063  ralprg  4076  rexprg  4077  difsn  4161  opthpr  4204  ralunsn  4233  csbuni  4273  dfiin2g  4358  iunxsng  4404  elpwuni  4413  disjxun  4445  sbcbr12g  4501  pwnss  4612  opthneg  4726  otthg  4730  opelopabt  4759  opelopabga  4760  brabga  4761  csbmpt12  4781  dfid3  4796  frirr  4856  wereu2  4876  ordtri4  4915  oneqmini  4929  elsucg  4945  elsuc2g  4946  brab2a  5048  opeliunxp  5050  posn  5067  sosn  5068  frsn  5069  brab2ga  5073  opbrop  5077  csbcnvgALT  5185  elrnmpt1  5249  elrnmptg  5250  eliniseg2  5374  poleloe  5399  xpdifid  5433  cnvpo  5543  sbcfung  5609  dffun8  5613  fncnv  5650  fununi  5652  fnssresb  5691  fnimaeq0  5700  funcocnv2  5838  csbfv12  5899  dffn5  5911  funimass4  5916  fnsnfv  5925  dmfco  5939  fndmdif  5983  fvimacnvi  5993  fvimacnvALT  5998  unpreima  6005  respreima  6008  fmptco  6052  fressnfv  6073  fmptsnd  6081  fnnfpeq0  6090  fnsuppresOLD  6119  elunirn  6149  dff13  6152  f12dfv  6165  f13dfv  6166  fliftel  6193  isoini  6220  f1oiso  6233  eloprabga  6371  resoprab2  6381  elrnmpt2res  6398  ralrnmpt2  6399  ovid  6401  ov  6404  ovg  6423  ofrfval2  6539  dfwe2  6595  ssonprc  6605  ordpwsuc  6628  dfom2  6680  f1oweALT  6765  el2xptp0  6825  fmpt2x  6847  ovmptss  6861  1stconst  6868  2ndconst  6869  fnsuppres  6924  isprmpt2  6950  brtpos2  6958  mpt2curryd  6995  dfsmo2  7015  rdglim2  7095  seqomlem2  7113  omeu  7231  oeeui  7248  brdifun  7335  eqerlem  7340  brecop  7401  erovlem  7404  eceqoveq  7413  mapsn  7457  ixpsnval  7469  mptelixpg  7503  map1  7591  xpsnen  7598  xpdom2  7609  omxpenlem  7615  xpf1o  7676  mapunen  7683  onfin  7705  fimaxg  7763  fodomfib  7796  fofinf1o  7797  fipreima  7822  supub  7915  ordtypecbv  7938  ordtypelem3  7941  ordtypelem9  7947  hartogslem1  7963  wofib  7966  wemapsolem  7971  wemapso2OLD  7973  wemapso2lem  7974  noinfep  8072  noinfepOLD  8073  cantnf  8108  cantnfOLD  8130  rankbnd2  8283  domtri2  8366  infxpenc2  8395  infxpenc2OLD  8399  fseqdom  8403  acni2  8423  dfac9  8512  cfeq0  8632  cfsuc  8633  cflim3  8638  cfslb  8642  cofsmo  8645  enfin2i  8697  isfin3ds  8705  isf33lem  8742  fin1a2lem5  8780  axdc2lem  8824  zorn2g  8879  fodomb  8900  brdom7disj  8905  brdom6disj  8906  iundom2g  8911  cfpwsdom  8955  elgch  8996  fpwwe2cbv  9004  fpwwecbv  9018  pwfseqlem3  9034  pwfseqlem4a  9035  pwfseqlem4  9036  ltpiord  9261  nlt1pi  9280  nqereu  9303  addclprlem1  9390  1idpr  9403  reclem3pr  9423  ltsosr  9467  map2psrpr  9483  supsrlem  9484  axrrecex  9536  xrlenlt  9648  eqlei2  9691  addsubeq4  9831  renegcli  9876  lesub0  10065  wloglei  10081  conjmul  10257  rereccl  10258  infm3  10498  supmul1  10504  supmullem1  10505  supmullem2  10506  supmul  10507  creui  10527  nndiv  10572  elznn0  10875  prime  10937  eqreznegel  11163  zsupss  11167  rebtwnz  11177  ltxr  11320  elixx3g  11538  ixxun  11541  ioo0  11550  ico0  11571  ioc0  11572  icc0  11573  difreicc  11648  divelunit  11658  iccf1o  11660  elfz2  11675  fzn  11698  fznn  11743  fzshftral  11761  fzosplitsni  11884  om2uzisoi  12028  rabssnn0fi  12058  mptnn0fsupp  12066  sq11i  12220  hashsdom  12411  euhash1  12439  brfi1uzind  12492  wrdval  12511  csbwrdg  12530  wrd2ind  12660  s2f1o  12821  cjreb  12913  rexfiuz  13136  cau3lem  13143  rlim2  13275  ello12  13295  ello1mpt  13300  elo12  13306  o1lo1  13316  lo1resb  13343  o1resb  13345  o1compt  13366  caucvgb  13458  mertens  13651  ruclem12  13828  divides  13842  odd2np1  13898  oddm1even  13899  sadadd2lem2  13952  gcdcllem2  14002  bezoutlem2  14029  bezoutlem3  14030  bezoutlem4  14031  isprm2  14077  isprm3  14078  prmreclem2  14287  prmreclem5  14290  prmreclem6  14291  4sqlem2  14319  4sqlem12  14326  vdwmc  14348  vdwpc  14350  vdwlem6  14356  vdwlem10  14360  vdwnn  14368  ramval  14378  0ram  14390  prdsleval  14725  pwsle  14740  imasleval  14789  xpsfrnel2  14813  xpsle  14829  isacs2  14901  mreacs  14906  acsfn  14907  iscatd2  14929  catpropd  14958  isssc  15043  evlfcl  15342  uncfcurf  15359  pltval  15440  lublecllem  15468  tosso  15516  oduleg  15612  oduclatb  15624  posglbmo  15627  isipodrs  15641  odudlatb  15676  gsumvalx  15812  grplmulf1o  15910  grplactcnv  15936  elnmz  16032  eqgid  16045  isghm  16059  ghmeqker  16085  resscntz  16161  symg1bas  16213  pgrpsubgsymgbi  16224  symgfixelq  16250  f1omvdconj  16264  odmulgeq  16372  sylow3lem3  16442  sylow3lem6  16445  efgval2  16535  efgsdm  16541  efgrelexlema  16560  efgcpbllemb  16566  iscyggen2  16672  cyggenod  16675  gsummptfzcl  16784  eldprd  16823  eldprdOLD  16825  dprdf11  16850  dprdf11OLD  16857  dprddisj2  16874  dprddisj2OLD  16875  pgpfac1lem2  16913  pgpfac1  16918  drngid2  17192  issubrg  17209  islmod  17296  aspval2  17764  psrbag  17781  cply1coe0bi  18110  zndvds  18352  znleval  18357  iunocv  18476  pjfval2  18504  pjdm2  18506  dsmmelbas  18534  ellspd  18600  ellspdOLD  18601  islindf  18611  islindf4  18637  istopg  19168  istpsOLD  19185  basgen2  19254  isclo  19351  mretopd  19356  isnei  19367  isperf3  19417  restdis  19442  neitr  19444  restcls  19445  restlp  19447  restperf  19448  iscn  19499  iscnp  19501  lmbr2  19523  lmbrf  19524  ordtt1  19643  cmpsub  19663  hauscmplem  19669  cmpfi  19671  bwthOLD  19674  dfcon2  19683  1stcelcls  19725  1stccn  19727  nllyi  19739  subislly  19745  elkgen  19769  ptpjpre1  19804  ptuni2  19809  ptclsg  19848  ptcnplem  19854  txcn  19859  hausdiag  19878  txhaus  19880  txkgen  19885  xkoptsub  19887  cnmpt21  19904  elqtop  19930  tgqtop  19945  r0cld  19971  elfg  20104  fbasrn  20117  trfil2  20120  trfil3  20121  fin1aufil  20165  elfm2  20181  elfm3  20183  flimopn  20208  fbflim  20209  flfnei  20224  flftg  20229  cnpflf2  20233  txflf  20239  fclsbas  20254  alexsubALTlem4  20282  cnextfvval  20297  snclseqg  20346  tgphaus  20347  tsmsfbas  20358  tsmssubm  20376  utopsnneip  20483  prdsxmetlem  20603  imasdsf1olem  20608  xpsdsval  20616  blres  20666  isxms2  20683  metcnp  20776  txmetcnp  20782  txmetcn  20783  metustelOLD  20786  metustel  20787  metuel2  20814  dscopn  20826  isngp4  20863  cnblcld  21014  metnrmlem1a  21094  icoopnst  21171  iocopnst  21172  elpi1  21277  lmmbr2  21430  cfil3i  21440  caucfil  21454  iscmet3  21464  lmclim  21473  metcld2  21477  bcthlem4  21498  minveclem3b  21575  minveclem6  21581  minveclem7  21582  ivthle  21600  ivthle2  21601  evthicc2  21604  ovolfioo  21611  ovolficc  21612  ovolgelb  21623  dyadmax  21739  subopnmbl  21745  ismbf3d  21793  mbfimaopnlem  21794  mbfimaopn2  21796  mbfaddlem  21799  mbfsup  21803  mbfinf  21804  i1f1lem  21828  i1fmulclem  21841  itg1climres  21853  mbfi1fseqlem4  21857  itg2monolem1  21889  itg2gt0  21899  isibl  21904  iblcnlem1  21926  ellimc2  22013  dvcnvrelem1  22150  itgsubst  22182  mdegleb  22196  fta1glem2  22299  quotval  22419  vieta1lem1  22437  vieta1lem2  22438  ulm2  22511  ulmcaulem  22520  ulmcau  22521  radcnvlt1  22544  sineq0  22644  cos11  22650  recosf1o  22652  efopn  22764  cxpeq  22856  mcubic  22903  birthdaylem3  23008  rlimcnp  23020  xrlimcnp  23023  wilth  23070  isppw  23113  isppw2  23114  mumullem2  23179  sqff1o  23181  dvdsmulf1o  23195  fsumvma  23213  fsumvma2  23214  vmasum  23216  chpchtsum  23219  lgsne0  23333  lgseisenlem2  23350  lgsquadlem1  23354  lgsquadlem2  23355  dchrmusumlema  23403  rpvmasum2  23422  dchrisum0lema  23424  pntibndlem3  23502  pntlemi  23514  pntleml  23521  pnt3  23522  trgcgrg  23631  colcom  23670  colrot1  23671  ltgov  23707  lncom  23713  mirreu3  23745  isperp  23794  perpcom  23795  brbtwn  23875  brcgr  23876  brbtwn2  23881  colinearalg  23886  axeuclidlem  23938  axcontlem2  23941  axcontlem4  23943  axcontlem7  23946  nbgraf1olem1  24114  nbgraf1olem5  24118  nbcusgra  24136  uvtx01vtx  24165  cusgrauvtxb  24169  iswlk  24193  istrl  24212  ispth  24243  isspth  24244  wlkdvspthlem  24282  usgrcyclnl2  24314  wwlkn0s  24378  wwlkextwrd  24401  wwlkextproplem3  24416  isclwlk0  24427  clwwlkn2  24448  eclclwwlkn1  24505  eleclclwwlkn  24506  hashecclwwlkn1  24507  usghashecclwwlk  24508  clwlkfclwwlk1hashn  24514  clwlkfoclwwlk  24518  usg2spthonot  24561  isrgra  24599  isrusgra  24600  isrusgusrg  24605  eupath2  24653  frgra3vlem2  24674  frgrancvvdeqlem2  24705  frgrancvvdeqlem3  24706  frgrancvvdeqlemC  24713  usg2spot2nb  24739  grpodiveq  24931  opidon  24997  issmgrp  25009  ismndo  25018  isrngo  25053  isdivrngo  25106  isvclem  25143  isnvlem  25176  isphg  25405  isph  25410  phoeqi  25446  ubthlem3  25461  minvecolem5  25470  minvecolem6  25471  minvecolem7  25472  hhph  25768  issh3  25810  nmopub  26500  nmfnleub  26517  adjeq  26527  adjvalval  26529  elunop2  26605  lnophm  26611  nmcexi  26618  cnlnadjlem5  26663  cnlnadjeui  26669  adjbd1o  26677  jpi  26862  mddmd2  26901  chrelati  26956  chrelat2i  26957  cvexchlem  26960  dmdbr5ati  27014  cdjreui  27024  cdj3i  27033  preqsnd  27089  disjunsn  27123  opeldifid  27126  fcoinvbr  27131  opabdm  27134  opabrn  27135  abfmpunirn  27159  feqmptdf  27170  fmptcof2  27171  ofpreima  27176  funcnvmptOLD  27178  funcnvmpt  27179  funcnv5mpt  27180  f1od2  27216  resf1o  27222  fpwrelmap  27225  negelrp  27229  iocinioc2  27255  eliccioo  27292  posrasymb  27304  isslmd  27404  pstmxmet  27509  prsdm  27529  prsrn  27530  ordtconlem1  27539  xrmulc1cn  27545  eulerpartlemmf  27951  isrrvv  28019  eldmgm  28201  dmgmaddn0  28202  lgamgulmlem6  28213  subfacp1lem3  28263  subfacp1lem6  28266  subfacp1  28267  txpcon  28314  sconpi1  28321  rescon  28328  cvmscbv  28340  cvmsval  28348  cvmlift2lem13  28397  cvmlift3lem2  28402  cvmlift3  28410  br8  28759  br6  28760  br4  28761  distel  28810  elpred  28831  poseq  28907  wsuclem  28955  sltsolem1  29002  imageval  29154  funpartfv  29169  dfrdg4  29174  altopthg  29191  altopthbg  29192  brcolinear2  29282  lineext  29300  brsegle  29332  seglelin  29340  broutsideof2  29346  onsuct0  29480  wl-sbrimt  29572  wl-sblimt  29573  wl-sbnf1  29577  wl-mo2dnae  29593  wl-mo2t  29594  wl-mo3t  29595  wl-ax11-lem6  29604  supaddc  29615  supadd  29616  tan2h  29622  ptrest  29623  mbfposadd  29637  cnambfre  29638  itg2addnclem2  29642  isfne4  29739  isfne2  29741  isfne3  29742  fneval  29757  topfneec  29761  neibastop2lem  29779  neibastop2  29780  neifg  29790  filnetlem4  29800  fdc  29839  heibor1  29907  rrncmslem  29929  rrnheibor  29934  isfldidl2  30067  isdmn3  30072  prtlem13  30211  prter3  30225  ellz1  30302  lzunuz  30303  fz1eqin  30304  diophrex  30311  rexrabdioph  30329  rexfrabdioph  30330  2rexfrabdioph  30331  3rexfrabdioph  30332  4rexfrabdioph  30333  6rexfrabdioph  30334  7rexfrabdioph  30335  fzneg  30522  expdioph  30569  wepwsolem  30591  fnwe2lem2  30601  islmodfg  30619  kercvrlsm  30633  sdrgacs  30755  pm10.52  30848  iotasbc  30904  pm14.122a  30907  pm14.122b  30908  pm14.123a  30910  rusbcALT  30924  fvsb  30939  stoweidlem34  31334  2reu4a  31661  funressnfv  31680  dfafn5a  31712  elfz2z  31800  usgra2pthlem1  31822  isuhgr  31835  isushgr  31836  usgo0s0ALT  31905  usgo1s0ALT  31906  ismgmALT  31925  iopmapxp  31960  ismgmALT2  31973  opeliun2xp  31986  snlindsntor  32145  gte-lte  32199  gt-lt  32200  trsbc  32391  bnj976  32915  bnj944  33075  bnj1173  33137  bnj1321  33162  bnj1373  33165  bnj1417  33176  bj-iftru  33233  bj-iffal  33234  bj-abbi  33442  bj-tagcg  33624  bj-projval  33635  lrelat  33811  islshpat  33814  lshpsmreu  33906  lkrpssN  33960  cmtvalN  34008  omllaw2N  34041  cvrval  34066  cvrval2  34071  cvlsupr3  34141  3dim0  34253  islln2  34307  islpln5  34331  islpln2  34332  islpln2ah  34345  islvol5  34375  islvol2  34376  4atlem11  34405  pmapglbx  34565  cdleme18d  35091  cdlemefrs29bpre0  35192  cdlemb3  35402  cdlemg33b  35503  cdlemkid3N  35729  cdlemkid4  35730  dvhb1dimN  35782  dia11N  35845  cdlemm10N  35915  dib11N  35957  dib1dim  35962  dibglbN  35963  diblsmopel  35968  dihopelvalcpre  36045  dih11  36062  dihmeetlem4preN  36103  dihmeetlem13N  36116  lcfrvalsnN  36338  lcfrlem9  36347  lcf1o  36348  mapdval4N  36429  baerlem3lem2  36507  baerlem5alem2  36508  baerlem5blem2  36509  hdmap1fval  36594  hdmapfval  36627  hdmapglem7a  36727  hlhillcs  36758