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  1445  had1  1447  ax12wdemo  1768  sbcomOLD  2118  sbal2  2175  abbi  2543  necon3abid  2631  necon3bid  2633  necon1abid  2654  r19.21t  2791  ceqsralt  2986  ralxpxfr2d  3073  ceqsrexv  3082  ceqsrex2v  3084  elab2g  3097  elrabf  3104  eueq2  3122  eqreu  3140  reu8  3144  ru  3174  sbcralt  3255  sbcabel  3263  sbcel1g  3669  sbcel2  3671  csbnestgf  3680  sbccsb2  3691  disjpss  3717  sbcssg  3778  rexsng  3901  ralprg  3913  rexprg  3914  difsn  3996  opthpr  4038  ralunsn  4067  csbuni  4107  dfiin2g  4191  iunxsng  4237  elpwuni  4246  disjxun  4278  sbcbr12g  4334  pwnss  4445  opthneg  4559  opelopabt  4590  opelopabga  4591  brabga  4592  dfid3  4624  frirr  4684  wereu2  4704  ordtri4  4743  oneqmini  4757  elsucg  4773  elsuc2g  4774  brab2a  4875  opeliunxp  4877  posn  4894  sosn  4895  frsn  4896  brab2ga  4899  opbrop  4903  csbcnvgOLD  5011  elrnmpt1  5075  elrnmptg  5076  eliniseg2  5196  poleloe  5220  xpdifid  5254  cnvpo  5363  sbcfung  5429  dffun8  5433  fncnv  5470  fununi  5472  fnssresb  5511  fnimaeq0  5520  funcocnv2  5653  csbfv12  5713  dffn5  5725  funimass4  5730  fnsnfv  5739  dmfco  5753  fndmdif  5795  fvimacnvi  5805  fvimacnvALT  5810  unpreima  5817  respreima  5820  fmptco  5863  fressnfv  5883  fnnfpeq0  5896  fnsuppresOLD  5925  elunirnALT  5957  dff13  5958  fliftel  5989  isoini  6016  f1oiso  6029  eloprabga  6166  resoprab2  6176  elrnmpt2res  6193  ralrnmpt2  6194  ovid  6196  ov  6199  ovg  6218  ofrfval2  6326  dfwe2  6382  ssonprc  6392  ordpwsuc  6415  dfom2  6467  f1oweALT  6550  fmpt2x  6629  ovmptss  6643  1stconst  6650  2ndconst  6651  fnsuppres  6705  isprmpt2  6732  brtpos2  6740  dfsmo2  6794  rdglim2  6874  seqomlem2  6892  omeu  7012  oeeui  7029  brdifun  7116  eqerlem  7121  brecop  7181  erovlem  7184  eceqoveq  7193  mapsn  7242  ixpsnval  7254  mptelixpg  7288  map1  7376  xpsnen  7383  xpdom2  7394  omxpenlem  7400  xpf1o  7461  mapunen  7468  onfin  7489  fimaxg  7547  fodomfib  7579  fofinf1o  7580  fipreima  7605  supub  7697  ordtypecbv  7719  ordtypelem3  7722  ordtypelem9  7728  hartogslem1  7744  wofib  7747  wemapsolem  7752  wemapso2OLD  7754  wemapso2lem  7755  noinfep  7853  noinfepOLD  7854  cantnf  7889  cantnfOLD  7911  rankbnd2  8064  domtri2  8147  infxpenc2  8176  infxpenc2OLD  8180  fseqdom  8184  acni2  8204  dfac9  8293  cfeq0  8413  cfsuc  8414  cflim3  8419  cfslb  8423  cofsmo  8426  enfin2i  8478  isfin3ds  8486  isf33lem  8523  fin1a2lem5  8561  axdc2lem  8605  zorn2g  8660  fodomb  8681  brdom7disj  8686  brdom6disj  8687  iundom2g  8692  cfpwsdom  8736  elgch  8777  fpwwe2cbv  8785  fpwwecbv  8799  pwfseqlem3  8815  pwfseqlem4a  8816  pwfseqlem4  8817  ltpiord  9044  nlt1pi  9063  nqereu  9086  addclprlem1  9173  1idpr  9186  reclem3pr  9206  ltsosr  9249  map2psrpr  9265  supsrlem  9266  axrrecex  9318  xrlenlt  9430  eqlei2  9473  addsubeq4  9613  renegcli  9658  lesub0  9844  wloglei  9860  conjmul  10036  rereccl  10037  infm3  10277  supmul1  10283  supmullem1  10284  supmullem2  10285  supmul  10286  creui  10305  nndiv  10350  elznn0  10649  prime  10710  eqreznegel  10928  zsupss  10932  rebtwnz  10940  ltxr  11083  elixx3g  11301  ixxun  11304  ioo0  11313  ico0  11334  ioc0  11335  icc0  11336  difreicc  11404  divelunit  11414  iccf1o  11416  elfz2  11431  fzn  11453  fznn  11510  fzshftral  11531  fzosplitsni  11618  om2uzisoi  11761  sq11i  11940  hashsdom  12128  euhash1  12156  brfi1uzind  12203  wrdval  12222  csbwrdg  12241  wrd2ind  12356  s2f1o  12510  cjreb  12596  rexfiuz  12819  cau3lem  12826  rlim2  12958  ello12  12978  ello1mpt  12983  elo12  12989  o1lo1  12999  lo1resb  13026  o1resb  13028  o1compt  13049  caucvgb  13141  mertens  13329  ruclem12  13506  divides  13520  odd2np1  13575  oddm1even  13576  sadadd2lem2  13629  gcdcllem2  13679  bezoutlem2  13706  bezoutlem3  13707  bezoutlem4  13708  isprm2  13754  isprm3  13755  prmreclem2  13961  prmreclem5  13964  prmreclem6  13965  4sqlem2  13993  4sqlem12  14000  vdwmc  14022  vdwpc  14024  vdwlem6  14030  vdwlem10  14034  vdwnn  14042  ramval  14052  0ram  14064  prdsleval  14398  pwsle  14413  imasleval  14462  xpsfrnel2  14486  xpsle  14502  isacs2  14574  mreacs  14579  acsfn  14580  iscatd2  14602  catpropd  14631  isssc  14716  evlfcl  15015  uncfcurf  15032  pltval  15113  lublecllem  15141  tosso  15189  oduleg  15285  oduclatb  15297  posglbmo  15300  isipodrs  15314  odudlatb  15349  gsumvalx  15484  grplmulf1o  15580  grplactcnv  15604  elnmz  15700  eqgid  15713  isghm  15727  ghmeqker  15753  resscntz  15829  symg1bas  15881  pgrpsubgsymgbi  15892  symgfixelq  15918  f1omvdconj  15932  odmulgeq  16038  sylow3lem3  16108  sylow3lem6  16111  efgval2  16201  efgsdm  16207  efgrelexlema  16226  efgcpbllemb  16232  iscyggen2  16338  cyggenod  16341  gsummptfzcl  16434  eldprd  16460  eldprdOLD  16462  dprdf11  16487  dprdf11OLD  16494  dprddisj2  16511  dprddisj2OLD  16512  pgpfac1lem2  16550  pgpfac1  16555  drngid2  16772  issubrg  16789  islmod  16876  aspval2  17339  psrbag  17365  zndvds  17824  znleval  17829  iunocv  17948  pjfval2  17976  pjdm2  17978  dsmmelbas  18006  ellspd  18072  ellspdOLD  18073  islindf  18083  islindf4  18109  istopg  18350  istpsOLD  18367  basgen2  18436  isclo  18533  mretopd  18538  isnei  18549  isperf3  18599  restdis  18624  neitr  18626  restcls  18627  restlp  18629  restperf  18630  iscn  18681  iscnp  18683  lmbr2  18705  lmbrf  18706  ordtt1  18825  cmpsub  18845  hauscmplem  18851  cmpfi  18853  bwthOLD  18856  dfcon2  18865  1stcelcls  18907  1stccn  18909  nllyi  18921  subislly  18927  elkgen  18951  ptpjpre1  18986  ptuni2  18991  ptclsg  19030  ptcnplem  19036  txcn  19041  hausdiag  19060  txhaus  19062  txkgen  19067  xkoptsub  19069  cnmpt21  19086  elqtop  19112  tgqtop  19127  r0cld  19153  elfg  19286  fbasrn  19299  trfil2  19302  trfil3  19303  fin1aufil  19347  elfm2  19363  elfm3  19365  flimopn  19390  fbflim  19391  flfnei  19406  flftg  19411  cnpflf2  19415  txflf  19421  fclsbas  19436  alexsubALTlem4  19464  cnextfvval  19479  snclseqg  19528  tgphaus  19529  tsmsfbas  19540  tsmssubm  19558  utopsnneip  19665  prdsxmetlem  19785  imasdsf1olem  19790  xpsdsval  19798  blres  19848  isxms2  19865  metcnp  19958  txmetcnp  19964  txmetcn  19965  metustelOLD  19968  metustel  19969  metuel2  19996  dscopn  20008  isngp4  20045  cnblcld  20196  metnrmlem1a  20276  icoopnst  20353  iocopnst  20354  elpi1  20459  lmmbr2  20612  cfil3i  20622  caucfil  20636  iscmet3  20646  lmclim  20655  metcld2  20659  bcthlem4  20680  minveclem3b  20757  minveclem6  20763  minveclem7  20764  ivthle  20782  ivthle2  20783  evthicc2  20786  ovolfioo  20793  ovolficc  20794  ovolgelb  20805  dyadmax  20920  subopnmbl  20926  ismbf3d  20974  mbfimaopnlem  20975  mbfimaopn2  20977  mbfaddlem  20980  mbfsup  20984  mbfinf  20985  i1f1lem  21009  i1fmulclem  21022  itg1climres  21034  mbfi1fseqlem4  21038  itg2monolem1  21070  itg2gt0  21080  isibl  21085  iblcnlem1  21107  ellimc2  21194  dvcnvrelem1  21331  itgsubst  21363  mdegleb  21420  fta1glem2  21523  quotval  21643  vieta1lem1  21661  vieta1lem2  21662  ulm2  21735  ulmcaulem  21744  ulmcau  21745  radcnvlt1  21768  sineq0  21868  cos11  21874  recosf1o  21876  efopn  21988  cxpeq  22080  mcubic  22127  birthdaylem3  22232  rlimcnp  22244  xrlimcnp  22247  wilth  22294  isppw  22337  isppw2  22338  mumullem2  22403  sqff1o  22405  dvdsmulf1o  22419  fsumvma  22437  fsumvma2  22438  vmasum  22440  chpchtsum  22443  lgsne0  22557  lgseisenlem2  22574  lgsquadlem1  22578  lgsquadlem2  22579  dchrmusumlema  22627  rpvmasum2  22646  dchrisum0lema  22648  pntibndlem3  22726  pntlemi  22738  pntleml  22745  pnt3  22746  trgcgrg  22848  colcom  22871  colrot1  22872  lncom  22903  mirreu3  22924  brbtwn  22968  brcgr  22969  brbtwn2  22974  colinearalg  22979  axeuclidlem  23031  axcontlem2  23034  axcontlem4  23036  axcontlem7  23039  nbgraf1olem1  23173  nbgraf1olem5  23177  nbcusgra  23194  uvtx01vtx  23223  cusgrauvtxb  23227  iswlk  23249  istrl  23259  ispth  23290  isspth  23291  wlkdvspthlem  23329  usgrcyclnl2  23350  eupath2  23424  grpodiveq  23566  opidon  23632  issmgrp  23644  ismndo  23653  isrngo  23688  isdivrngo  23741  isvclem  23778  isnvlem  23811  isphg  24040  isph  24045  phoeqi  24081  ubthlem3  24096  minvecolem5  24105  minvecolem6  24106  minvecolem7  24107  hhph  24403  issh3  24445  nmopub  25135  nmfnleub  25152  adjeq  25162  adjvalval  25164  elunop2  25240  lnophm  25246  nmcexi  25253  cnlnadjlem5  25298  cnlnadjeui  25304  adjbd1o  25312  jpi  25497  mddmd2  25536  chrelati  25591  chrelat2i  25592  cvexchlem  25595  dmdbr5ati  25649  cdjreui  25659  cdj3i  25668  preqsnd  25725  disjunsn  25760  opabdm  25767  opabrn  25768  abfmpunirn  25791  feqmptdf  25802  fmptcof2  25803  ofpreima  25808  funcnvmptOLD  25810  funcnvmpt  25811  funcnv5mpt  25812  f1od2  25848  resf1o  25855  fpwrelmap  25858  negelrp  25862  iocinioc2  25892  eliccioo  25929  posrasymb  25941  isslmd  26067  pstmxmet  26178  prsdm  26198  prsrn  26199  ordtconlem1  26208  xrmulc1cn  26214  isrrvv  26674  eldmgm  26856  dmgmaddn0  26857  lgamgulmlem6  26868  subfacp1lem3  26918  subfacp1lem6  26921  subfacp1  26922  txpcon  26969  sconpi1  26976  rescon  26983  cvmscbv  26995  cvmsval  27003  cvmlift2lem13  27052  cvmlift3lem2  27057  cvmlift3  27065  br8  27413  br6  27414  br4  27415  distel  27464  elpred  27485  poseq  27561  wsuclem  27609  sltsolem1  27656  imageval  27808  funpartfv  27823  dfrdg4  27828  altopthg  27845  altopthbg  27846  brcolinear2  27936  lineext  27954  brsegle  27986  seglelin  27994  broutsideof2  28000  onsuct0  28135  wl-sbrimt  28222  wl-sblimt  28223  wl-sbnf1  28227  wl-mo2dnae  28239  wl-mo2t  28240  wl-mo3t  28241  wl-ax11-lem6  28250  supaddc  28261  supadd  28262  tan2h  28268  ptrest  28269  mbfposadd  28283  cnambfre  28284  itg2addnclem2  28288  isfne4  28385  isfne2  28387  isfne3  28388  fneval  28403  topfneec  28407  neibastop2lem  28425  neibastop2  28426  neifg  28436  filnetlem4  28446  fdc  28485  heibor1  28553  rrncmslem  28575  rrnheibor  28580  isfldidl2  28713  isdmn3  28718  prtlem13  28858  prter3  28872  ellz1  28950  lzunuz  28951  fz1eqin  28952  diophrex  28959  rexrabdioph  28977  rexfrabdioph  28978  2rexfrabdioph  28979  3rexfrabdioph  28980  4rexfrabdioph  28981  6rexfrabdioph  28982  7rexfrabdioph  28983  fzneg  29170  expdioph  29217  wepwsolem  29239  fnwe2lem2  29249  islmodfg  29267  kercvrlsm  29281  sdrgacs  29403  pm10.52  29462  iotasbc  29518  pm14.122a  29521  pm14.122b  29522  pm14.123a  29524  rusbcALT  29538  fvsb  29553  stoweidlem34  29675  2reu4a  29859  funressnfv  29880  dfafn5a  29912  el2xptp0  29973  otthg  29976  f12dfv  29992  f13dfv  29993  elfz2z  30044  usgra2pthlem1  30146  wwlkn0s  30185  wwlkextwrd  30206  usg2spthonot  30253  isclwlk0  30265  clwwlkn2  30284  eclclwwlkn1  30352  eleclclwwlkn  30353  hashecclwwlkn1  30354  usghashecclwwlk  30355  clwlkfclwwlk1hashn  30360  clwlkfoclwwlk  30364  isrgra  30389  isrusgra  30390  wwlkextproplem3  30408  frgra3vlem2  30439  frgrancvvdeqlem2  30470  frgrancvvdeqlem3  30471  frgrancvvdeqlemC  30478  usg2spot2nb  30504  opeliun2xp  30565  fmptsnd  30567  snlindsntor  30714  gte-lte  30768  gt-lt  30769  trsbc  30948  bnj976  31473  bnj944  31633  bnj1173  31695  bnj1321  31720  bnj1373  31723  bnj1417  31734  bj-abbi  31918  bj-tagcg  32061  bj-projval  32072  lrelat  32232  islshpat  32235  lshpsmreu  32327  lkrpssN  32381  cmtvalN  32429  omllaw2N  32462  cvrval  32487  cvrval2  32492  cvlsupr3  32562  3dim0  32674  islln2  32728  islpln5  32752  islpln2  32753  islpln2ah  32766  islvol5  32796  islvol2  32797  4atlem11  32826  pmapglbx  32986  cdleme18d  33512  cdlemefrs29bpre0  33613  cdlemb3  33823  cdlemg33b  33924  cdlemkid3N  34150  cdlemkid4  34151  dvhb1dimN  34203  dia11N  34266  cdlemm10N  34336  dib11N  34378  dib1dim  34383  dibglbN  34384  diblsmopel  34389  dihopelvalcpre  34466  dih11  34483  dihmeetlem4preN  34524  dihmeetlem13N  34537  lcfrvalsnN  34759  lcfrlem9  34768  lcf1o  34769  mapdval4N  34850  baerlem3lem2  34928  baerlem5alem2  34929  baerlem5blem2  34930  hdmap1fval  35015  hdmapfval  35048  hdmapglem7a  35148  hlhillcs  35179