Theorem syl5bb 260

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 256	1 |- ( ch -> ( ph <-> th ) )

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

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 188

This theorem is referenced by:  syl5rbb  261  syl5bbr  262  3bitr4g  291  imim21b  368  ifpfal  1432  cad0  1515  ax12wdemo  1883  sbal2  2257  abbiOLD  2561  necon3abid  2677  necon1abidOLD  2680  necon3bid  2689  r19.21tOLD  2830  ceqsralt  3111  ralxpxfr2d  3202  ceqsrexv  3211  ceqsrex2v  3213  elab2g  3226  elrabf  3233  elrab3t  3234  eueq2  3251  eqreu  3269  reu8  3273  ru  3304  sbcralt  3378  sbcabel  3383  sbcel1g  3810  sbcel2  3812  csbnestgf  3819  sbccsb2  3828  disjpss  3849  sbcssg  3914  rexsng  4038  ralprg  4052  rexprg  4053  difsn  4137  opthpr  4181  ralunsn  4210  csbuni  4250  dfiin2g  4335  iunxsng  4384  elpwuni  4393  disjxun  4424  sbcbr12g  4479  pwnss  4590  opthneg  4701  otthg  4705  opelopabt  4733  opelopabga  4734  brabga  4735  csbmpt12  4755  dfid3  4770  frirr  4831  wereu2  4851  brab2a  4904  opeliunxp  4906  posn  4923  sosn  4924  frsn  4925  brab2ga  4930  opbrop  4934  csbcnvgALT  5039  elrnmpt1  5103  elrnmptg  5104  eliniseg2  5229  poleloe  5251  xpdifid  5285  cnvpo  5394  elpred  5412  ordtri4  5479  oneqmini  5493  elsucg  5509  elsuc2g  5510  sbcfung  5624  dffun8  5628  fncnv  5665  fununi  5667  fnssresb  5706  fnimaeq0  5715  funcocnv2  5855  csbfv12  5916  dffn5  5926  funimass4  5932  fnsnfv  5941  dmfco  5955  fndmdif  6001  fvimacnvi  6011  fvimacnvALT  6016  unpreima  6021  respreima  6024  fmptco  6071  fressnfv  6093  fmptsnd  6101  fnnfpeq0  6110  tpres  6132  elunirn  6171  dff13  6174  f12dfv  6187  f13dfv  6188  fliftel  6217  isoini  6244  f1oiso  6257  eloprabga  6397  resoprab2  6407  elrnmpt2res  6424  ralrnmpt2  6425  ovid  6427  ov  6430  ovg  6449  ofrfval2  6563  dfwe2  6622  ssonprc  6633  ordpwsuc  6656  dfom2  6708  f1oweALT  6791  el2xptp0  6851  fmpt2x  6873  ovmptss  6888  1stconst  6895  2ndconst  6896  fnsuppres  6953  isprmpt2  6979  brtpos2  6987  mpt2curryd  7024  dfsmo2  7074  rdglim2  7158  seqomlem2  7176  omeu  7294  oeeui  7311  brdifun  7398  eqerlem  7403  brecop  7464  erovlem  7467  eceqoveq  7476  mapsn  7521  ixpsnval  7533  mptelixpg  7567  map1  7655  xpsnen  7662  xpdom2  7673  omxpenlem  7679  xpf1o  7740  mapunen  7747  onfin  7769  fimaxg  7824  fodomfib  7857  fofinf1o  7858  fipreima  7886  supub  7979  infglb  8012  infglbb  8013  ordtypecbv  8032  ordtypelem3  8035  ordtypelem9  8041  hartogslem1  8057  wofib  8060  wemapsolem  8065  wemapso2lem  8067  noinfep  8164  cantnf  8197  rankbnd2  8339  domtri2  8422  infxpenc2  8451  fseqdom  8455  acni2  8475  dfac9  8564  cfeq0  8684  cfsuc  8685  cflim3  8690  cfslb  8694  cofsmo  8697  enfin2i  8749  isfin3ds  8757  isf33lem  8794  fin1a2lem5  8832  axdc2lem  8876  zorn2g  8931  fodomb  8952  brdom7disj  8957  brdom6disj  8958  iundom2g  8963  cfpwsdom  9007  elgch  9046  fpwwe2cbv  9054  fpwwecbv  9068  pwfseqlem3  9084  pwfseqlem4a  9085  pwfseqlem4  9086  ltpiord  9311  nlt1pi  9330  nqereu  9353  addclprlem1  9440  1idpr  9453  reclem3pr  9473  ltsosr  9517  map2psrpr  9533  supsrlem  9534  axrrecex  9586  xrlenlt  9698  eqlei2  9744  addsubeq4  9889  renegcli  9934  lesub0  10130  wloglei  10145  conjmul  10323  rereccl  10324  infm3  10568  supaddc  10574  supadd  10575  supmul1  10576  supmullem1  10577  supmullem2  10578  supmul  10579  creui  10604  nndiv  10650  elznn0  10952  prime  11016  eqreznegel  11249  zsupss  11253  rebtwnz  11263  negelrp  11333  ltxr  11415  elixx3g  11648  ixxun  11651  ioo0  11661  ico0  11682  ioc0  11683  icc0  11684  difreicc  11762  divelunit  11772  iccf1o  11774  elfz2  11789  fzn  11813  fznn  11861  fzshftral  11880  nelfzo  11923  fzosplitsni  12016  om2uzisoi  12165  rabssnn0fi  12195  mptnn0fsupp  12206  sq11i  12362  hashsdom  12557  brfi1uzind  12641  wrdval  12661  csbwrdg  12683  wrd2ind  12819  s2f1o  12980  cjreb  13165  rexfiuz  13389  cau3lem  13396  rlim2  13538  ello12  13558  ello1mpt  13563  elo12  13569  o1lo1  13579  lo1resb  13606  o1resb  13608  o1compt  13629  caucvgb  13724  mertens  13920  ruclem12  14271  divides  14285  odd2np1  14343  oddm1even  14344  sadadd2lem2  14398  gcdcllem2  14448  bezoutlem2  14478  bezoutlem3  14479  bezoutlem4  14480  isprm2  14594  isprm3  14595  prmreclem2  14815  prmreclem5  14818  prmreclem6  14819  4sqlem2  14847  4sqlem12  14854  vdwmc  14882  vdwpc  14884  vdwlem6  14890  vdwlem10  14894  vdwnn  14902  ramval  14914  ramvalOLD  14915  0ram  14932  prdsleval  15325  pwsle  15340  imasleval  15389  xpsfrnel2  15413  xpsle  15429  isacs2  15501  mreacs  15506  acsfn  15507  iscatd2  15529  catpropd  15556  ciclcl  15649  cicrcl  15650  isssc  15667  evlfcl  16049  uncfcurf  16066  pltval  16148  lublecllem  16176  tosso  16224  oduleg  16320  oduclatb  16332  posglbmo  16335  isipodrs  16349  odudlatb  16384  gsumvalx  16455  sgrp2rid2  16602  grplmulf1o  16670  grplactcnv  16696  elnmz  16798  eqgid  16811  isghm  16825  ghmeqker  16851  resscntz  16927  symg1bas  16979  pgrpsubgsymgbi  16990  symgfixelq  17016  f1omvdconj  17029  odmulgeq  17137  sylow3lem3  17207  sylow3lem6  17210  efgval2  17300  efgsdm  17306  efgrelexlema  17325  efgcpbllemb  17331  iscyggen2  17442  cyggenod  17445  gsummptfzcl  17527  eldprd  17562  dprdf11  17582  dprddisj2  17598  pgpfac1lem2  17634  pgpfac1  17639  srg1zr  17688  drngid2  17917  issubrg  17934  islmod  18021  aspval2  18497  psrbag  18514  cply1coe0bi  18820  zndvds  19042  znleval  19047  iunocv  19166  pjfval2  19194  pjdm2  19196  dsmmelbas  19224  ellspd  19282  islindf  19292  islindf4  19318  istopg  19847  basgen2  19927  isclo  20025  mretopd  20030  isnei  20041  isperf3  20091  restdis  20116  neitr  20118  restcls  20119  restlp  20121  restperf  20122  iscn  20173  iscnp  20175  lmbr2  20197  lmbrf  20198  ordtt1  20317  cmpsub  20337  hauscmplem  20343  cmpfi  20345  dfcon2  20356  1stcelcls  20398  1stccn  20400  nllyi  20412  subislly  20418  dissnlocfin  20466  elkgen  20473  ptpjpre1  20508  ptuni2  20513  ptclsg  20552  ptcnplem  20558  txcn  20563  hausdiag  20582  txhaus  20584  txkgen  20589  xkoptsub  20591  cnmpt21  20608  elqtop  20634  tgqtop  20649  r0cld  20675  elfg  20808  fbasrn  20821  trfil2  20824  trfil3  20825  fin1aufil  20869  elfm2  20885  elfm3  20887  flimopn  20912  fbflim  20913  flfnei  20928  flftg  20933  cnpflf2  20937  txflf  20943  fclsbas  20958  alexsubALTlem4  20987  cnextfvval  21002  snclseqg  21052  tgphaus  21053  tsmsfbas  21064  tsmssubm  21079  utopsnneip  21185  prdsxmetlem  21305  imasdsf1olem  21310  xpsdsval  21318  blres  21368  isxms2  21385  metcnp  21478  txmetcnp  21484  txmetcn  21485  metustel  21487  metuel2  21502  dscopn  21510  isngp4  21547  cnblcld  21697  metnrmlem1a  21777  icoopnst  21854  iocopnst  21855  elpi1  21960  lmmbr2  22113  cfil3i  22123  caucfil  22137  iscmet3  22147  lmclim  22156  metcld2  22160  bcthlem4  22179  minveclem3b  22254  minveclem6  22260  minveclem7  22261  ivthle  22279  ivthle2  22280  evthicc2  22283  ovolfioo  22290  ovolficc  22291  ovolgelb  22302  dyadmax  22424  subopnmbl  22430  ismbf3d  22478  mbfimaopnlem  22479  mbfimaopn2  22481  mbfaddlem  22484  mbfsup  22488  mbfinf  22489  mbfinfOLD  22490  i1f1lem  22515  i1fmulclem  22528  itg1climres  22540  mbfi1fseqlem4  22544  itg2monolem1  22576  itg2gt0  22586  isibl  22591  iblcnlem1  22613  ellimc2  22700  dvcnvrelem1  22837  itgsubst  22869  mdegleb  22881  fta1glem2  22983  quotval  23104  vieta1lem1  23122  vieta1lem2  23123  ulm2  23196  ulmcaulem  23205  ulmcau  23206  radcnvlt1  23229  sineq0  23332  cos11  23338  recosf1o  23340  efopn  23459  cxpeq  23553  mcubic  23629  birthdaylem3  23735  rlimcnp  23747  xrlimcnp  23750  eldmgm  23803  dmgmaddn0  23804  lgamgulmlem6  23815  wilth  23852  isppw  23895  isppw2  23896  mumullem2  23961  sqff1o  23963  dvdsmulf1o  23977  fsumvma  23995  fsumvma2  23996  vmasum  23998  chpchtsum  24001  lgsne0  24115  lgseisenlem2  24132  lgsquadlem1  24136  lgsquadlem2  24137  dchrmusumlema  24185  rpvmasum2  24204  dchrisum0lema  24206  pntibndlem3  24284  pntlemi  24296  pntleml  24303  pnt3  24304  trgcgrg  24413  colcom  24454  colrot1  24455  ltgov  24493  hlcomb  24499  lncom  24517  mirreu3  24550  isperp  24605  perpcom  24606  brbtwn  24766  brcgr  24767  brbtwn2  24772  colinearalg  24777  axeuclidlem  24829  axcontlem2  24832  axcontlem4  24834  axcontlem7  24837  nbgraf1olem1  25005  nbgraf1olem5  25009  nbcusgra  25027  uvtx01vtx  25056  cusgrauvtxb  25060  iswlk  25084  istrl  25103  ispth  25134  isspth  25135  wlkdvspthlem  25173  usgrcyclnl2  25205  wwlkn0s  25269  wwlkextwrd  25292  wwlkextproplem3  25307  isclwlk0  25318  clwwlkn2  25339  eclclwwlkn1  25396  eleclclwwlkn  25397  hashecclwwlkn1  25398  usghashecclwwlk  25399  clwlkfclwwlk1hashn  25405  clwlkfoclwwlk  25409  usg2spthonot  25452  isrgra  25490  isrusgra  25491  isrusgusrg  25496  eupath2  25544  frgra3vlem2  25565  frgrancvvdeqlem2  25595  frgrancvvdeqlem3  25596  frgrancvvdeqlemC  25603  usg2spot2nb  25629  grpodiveq  25820  opidonOLD  25886  issmgrpOLD  25898  ismndo  25907  isrngo  25942  isdivrngo  25995  isvclem  26032  isnvlem  26065  isphg  26294  isph  26299  phoeqi  26335  ubthlem3  26350  minvecolem5  26359  minvecolem6  26360  minvecolem7  26361  hhph  26657  issh3  26698  nmopub  27387  nmfnleub  27404  adjeq  27414  adjvalval  27416  elunop2  27492  lnophm  27498  nmcexi  27505  cnlnadjlem5  27550  cnlnadjeui  27556  adjbd1o  27564  jpi  27749  mddmd2  27788  chrelati  27843  chrelat2i  27844  cvexchlem  27847  dmdbr5ati  27901  cdjreui  27911  cdj3i  27920  preqsnd  27987  iunxsngf  28002  disjunsn  28034  opeldifid  28040  fcoinvbr  28045  brabgaf  28046  opabdm  28049  opabrn  28050  iunsnima  28055  abfmpunirn  28082  feqmptdf  28089  fmptcof2  28090  funcnvmptOLD  28101  funcnvmpt  28102  funcnv5mpt  28103  f1od2  28143  resf1o  28149  fpwrelmap  28152  iocinioc2  28188  eliccioo  28229  posrasymb  28247  isslmd  28347  smatrcl  28452  pstmxmet  28530  prsdm  28550  prsrn  28551  ordtconlem1  28560  xrmulc1cn  28566  ispisys2  28805  elcarsg  28957  eulerpartlemmf  29025  isrrvv  29093  bnj976  29368  bnj944  29528  bnj1173  29590  bnj1321  29615  bnj1373  29618  bnj1417  29629  subfacp1lem3  29684  subfacp1lem6  29687  subfacp1  29688  txpcon  29734  sconpi1  29741  rescon  29748  cvmscbv  29760  cvmsval  29768  cvmlift2lem13  29817  cvmlift3lem2  29822  cvmlift3  29830  mclsrcl  29978  br8  30174  br6  30175  br4  30176  fv1stcnv  30200  fv2ndcnv  30201  distel  30228  poseq  30269  wsuclem  30286  sltsolem1  30333  imageval  30473  funpartfv  30488  dfrdg4  30494  altopthg  30510  altopthbg  30511  brcolinear2  30601  lineext  30619  brsegle  30651  seglelin  30659  broutsideof2  30665  isfne4  30772  isfne2  30774  isfne3  30775  fneval  30784  topfneec  30787  neibastop2lem  30792  neibastop2  30793  neifg  30803  filnetlem4  30813  onsuct0  30877  bj-abbi  31132  bj-tagcg  31319  bj-projval  31330  topdifinffinlem  31475  isbasisrelowllem1  31483  isbasisrelowllem2  31484  wl-sbrimt  31576  wl-sblimt  31577  wl-sbnf1  31581  wl-mo2dnae  31597  wl-mo2t  31598  wl-mo3t  31599  wl-ax11-lem6  31614  tan2h  31631  ptrest  31633  poimirlem2  31636  poimirlem16  31650  poimirlem19  31653  poimirlem23  31657  poimirlem24  31658  poimirlem25  31659  poimirlem26  31660  poimirlem27  31661  mbfposadd  31682  cnambfre  31683  itg2addnclem2  31688  fdc  31768  heibor1  31836  rrncmslem  31858  rrnheibor  31863  isfldidl2  31996  isdmn3  32001  prtlem13  32138  prter3  32152  lrelat  32279  islshpat  32282  lshpsmreu  32374  lkrpssN  32428  cmtvalN  32476  omllaw2N  32509  cvrval  32534  cvrval2  32539  cvlsupr3  32609  3dim0  32721  islln2  32775  islpln5  32799  islpln2  32800  islpln2ah  32813  islvol5  32843  islvol2  32844  4atlem11  32873  pmapglbx  33033  cdleme18d  33560  cdlemefrs29bpre0  33662  cdlemb3  33872  cdlemg33b  33973  cdlemkid3N  34199  cdlemkid4  34200  dvhb1dimN  34252  dia11N  34315  cdlemm10N  34385  dib11N  34427  dib1dim  34432  dibglbN  34433  diblsmopel  34438  dihopelvalcpre  34515  dih11  34532  dihmeetlem4preN  34573  dihmeetlem13N  34586  lcfrvalsnN  34808  lcfrlem9  34817  lcf1o  34818  mapdval4N  34899  baerlem3lem2  34977  baerlem5alem2  34978  baerlem5blem2  34979  hdmap1fval  35064  hdmapfval  35097  hdmapglem7a  35197  hlhillcs  35228  ellz1  35308  lzunuz  35309  fz1eqin  35310  diophrex  35317  rexrabdioph  35336  rexfrabdioph  35337  2rexfrabdioph  35338  3rexfrabdioph  35339  4rexfrabdioph  35340  6rexfrabdioph  35341  7rexfrabdioph  35342  fzneg  35528  expdioph  35574  wepwsolem  35596  fnwe2lem2  35605  islmodfg  35623  kercvrlsm  35637  sdrgacs  35756  iunrelexpuztr  35940  brtrclfv2  35948  frege124d  35982  pm10.52  36341  iotasbc  36397  pm14.122a  36400  pm14.122b  36401  pm14.123a  36403  rusbcALT  36417  fvsb  36432  trsbc  36528  rexsngf  37022  iunxsngf2  37034  limcperiod  37270  limsupre  37283  limsupreOLD  37284  dvbdfbdioo  37364  stoweidlem34  37454  fourierdlem108  37636  fourierdlem110  37638  etransc  37705  2reu4a  37991  funressnfv  38010  dfafn5a  38042  el1fzopredsuc  38102  iccelpart  38127  dfeven2  38159  gboge7  38244  bgoldbwt  38258  elfz2z  38394  usgra2pthlem1  38413  isuhgr  38426  isushgr  38427  usgo0s0ALT  38496  usgo1s0ALT  38497  ismhm0  38553  inclfusubc  38615  isrnghm  38640  rnghmval2  38643  uzlidlring  38677  lidldomnnring  38678  zrninitoringc  38821  opeliun2xp  38864  snlindsntor  39014  elbigo2  39114  gte-lte  39195  gt-lt  39196