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  1443  had1  1445  ax12wdemo  1771  sbal2  2180  abbiOLD  2583  necon3abid  2694  necon1abidOLD  2697  necon3bid  2706  r19.21t  2897  ceqsralt  3092  ralxpxfr2d  3181  ceqsrexv  3190  ceqsrex2v  3192  elab2g  3205  elrabf  3212  eueq2  3230  eqreu  3248  reu8  3252  ru  3283  sbcralt  3365  sbcabel  3373  sbcel1g  3779  sbcel2  3781  csbnestgf  3790  sbccsb2  3801  disjpss  3827  sbcssg  3888  rexsng  4011  ralprg  4023  rexprg  4024  difsn  4106  opthpr  4148  ralunsn  4177  csbuni  4217  dfiin2g  4301  iunxsng  4347  elpwuni  4356  disjxun  4388  sbcbr12g  4444  pwnss  4555  opthneg  4669  opelopabt  4699  opelopabga  4700  brabga  4701  csbmpt12  4720  dfid3  4735  frirr  4795  wereu2  4815  ordtri4  4854  oneqmini  4868  elsucg  4884  elsuc2g  4885  brab2a  4986  opeliunxp  4988  posn  5005  sosn  5006  frsn  5007  brab2ga  5010  opbrop  5014  csbcnvgALT  5122  elrnmpt1  5186  elrnmptg  5187  eliniseg2  5306  poleloe  5330  xpdifid  5364  cnvpo  5473  sbcfung  5539  dffun8  5543  fncnv  5580  fununi  5582  fnssresb  5621  fnimaeq0  5630  funcocnv2  5763  csbfv12  5824  dffn5  5836  funimass4  5841  fnsnfv  5850  dmfco  5864  fndmdif  5906  fvimacnvi  5916  fvimacnvALT  5921  unpreima  5928  respreima  5931  fmptco  5975  fressnfv  5995  fnnfpeq0  6008  fnsuppresOLD  6037  elunirn  6067  dff13  6070  fliftel  6101  isoini  6128  f1oiso  6141  eloprabga  6277  resoprab2  6287  elrnmpt2res  6304  ralrnmpt2  6305  ovid  6307  ov  6310  ovg  6329  ofrfval2  6437  dfwe2  6493  ssonprc  6503  ordpwsuc  6526  dfom2  6578  f1oweALT  6661  fmpt2x  6740  ovmptss  6754  1stconst  6761  2ndconst  6762  fnsuppres  6816  isprmpt2  6843  brtpos2  6851  mpt2curryd  6888  dfsmo2  6908  rdglim2  6988  seqomlem2  7006  omeu  7124  oeeui  7141  brdifun  7228  eqerlem  7233  brecop  7293  erovlem  7296  eceqoveq  7305  mapsn  7354  ixpsnval  7366  mptelixpg  7400  map1  7488  xpsnen  7495  xpdom2  7506  omxpenlem  7512  xpf1o  7573  mapunen  7580  onfin  7602  fimaxg  7660  fodomfib  7692  fofinf1o  7693  fipreima  7718  supub  7810  ordtypecbv  7832  ordtypelem3  7835  ordtypelem9  7841  hartogslem1  7857  wofib  7860  wemapsolem  7865  wemapso2OLD  7867  wemapso2lem  7868  noinfep  7966  noinfepOLD  7967  cantnf  8002  cantnfOLD  8024  rankbnd2  8177  domtri2  8260  infxpenc2  8289  infxpenc2OLD  8293  fseqdom  8297  acni2  8317  dfac9  8406  cfeq0  8526  cfsuc  8527  cflim3  8532  cfslb  8536  cofsmo  8539  enfin2i  8591  isfin3ds  8599  isf33lem  8636  fin1a2lem5  8674  axdc2lem  8718  zorn2g  8773  fodomb  8794  brdom7disj  8799  brdom6disj  8800  iundom2g  8805  cfpwsdom  8849  elgch  8890  fpwwe2cbv  8898  fpwwecbv  8912  pwfseqlem3  8928  pwfseqlem4a  8929  pwfseqlem4  8930  ltpiord  9157  nlt1pi  9176  nqereu  9199  addclprlem1  9286  1idpr  9299  reclem3pr  9319  ltsosr  9362  map2psrpr  9378  supsrlem  9379  axrrecex  9431  xrlenlt  9543  eqlei2  9586  addsubeq4  9726  renegcli  9771  lesub0  9957  wloglei  9973  conjmul  10149  rereccl  10150  infm3  10390  supmul1  10396  supmullem1  10397  supmullem2  10398  supmul  10399  creui  10418  nndiv  10463  elznn0  10762  prime  10823  eqreznegel  11041  zsupss  11045  rebtwnz  11053  ltxr  11196  elixx3g  11414  ixxun  11417  ioo0  11426  ico0  11447  ioc0  11448  icc0  11449  difreicc  11518  divelunit  11528  iccf1o  11530  elfz2  11545  fzn  11567  fznn  11627  fzshftral  11648  fzosplitsni  11735  om2uzisoi  11878  sq11i  12057  hashsdom  12246  euhash1  12274  brfi1uzind  12321  wrdval  12340  csbwrdg  12359  wrd2ind  12474  s2f1o  12628  cjreb  12714  rexfiuz  12937  cau3lem  12944  rlim2  13076  ello12  13096  ello1mpt  13101  elo12  13107  o1lo1  13117  lo1resb  13144  o1resb  13146  o1compt  13167  caucvgb  13259  mertens  13448  ruclem12  13625  divides  13639  odd2np1  13694  oddm1even  13695  sadadd2lem2  13748  gcdcllem2  13798  bezoutlem2  13825  bezoutlem3  13826  bezoutlem4  13827  isprm2  13873  isprm3  13874  prmreclem2  14080  prmreclem5  14083  prmreclem6  14084  4sqlem2  14112  4sqlem12  14119  vdwmc  14141  vdwpc  14143  vdwlem6  14149  vdwlem10  14153  vdwnn  14161  ramval  14171  0ram  14183  prdsleval  14517  pwsle  14532  imasleval  14581  xpsfrnel2  14605  xpsle  14621  isacs2  14693  mreacs  14698  acsfn  14699  iscatd2  14721  catpropd  14750  isssc  14835  evlfcl  15134  uncfcurf  15151  pltval  15232  lublecllem  15260  tosso  15308  oduleg  15404  oduclatb  15416  posglbmo  15419  isipodrs  15433  odudlatb  15468  gsumvalx  15604  grplmulf1o  15702  grplactcnv  15726  elnmz  15822  eqgid  15835  isghm  15849  ghmeqker  15875  resscntz  15951  symg1bas  16003  pgrpsubgsymgbi  16014  symgfixelq  16040  f1omvdconj  16054  odmulgeq  16162  sylow3lem3  16232  sylow3lem6  16235  efgval2  16325  efgsdm  16331  efgrelexlema  16350  efgcpbllemb  16356  iscyggen2  16462  cyggenod  16465  gsummptfzcl  16565  eldprd  16591  eldprdOLD  16593  dprdf11  16618  dprdf11OLD  16625  dprddisj2  16642  dprddisj2OLD  16643  pgpfac1lem2  16681  pgpfac1  16686  drngid2  16954  issubrg  16971  islmod  17058  aspval2  17523  psrbag  17537  zndvds  18091  znleval  18096  iunocv  18215  pjfval2  18243  pjdm2  18245  dsmmelbas  18273  ellspd  18339  ellspdOLD  18340  islindf  18350  islindf4  18376  istopg  18624  istpsOLD  18641  basgen2  18710  isclo  18807  mretopd  18812  isnei  18823  isperf3  18873  restdis  18898  neitr  18900  restcls  18901  restlp  18903  restperf  18904  iscn  18955  iscnp  18957  lmbr2  18979  lmbrf  18980  ordtt1  19099  cmpsub  19119  hauscmplem  19125  cmpfi  19127  bwthOLD  19130  dfcon2  19139  1stcelcls  19181  1stccn  19183  nllyi  19195  subislly  19201  elkgen  19225  ptpjpre1  19260  ptuni2  19265  ptclsg  19304  ptcnplem  19310  txcn  19315  hausdiag  19334  txhaus  19336  txkgen  19341  xkoptsub  19343  cnmpt21  19360  elqtop  19386  tgqtop  19401  r0cld  19427  elfg  19560  fbasrn  19573  trfil2  19576  trfil3  19577  fin1aufil  19621  elfm2  19637  elfm3  19639  flimopn  19664  fbflim  19665  flfnei  19680  flftg  19685  cnpflf2  19689  txflf  19695  fclsbas  19710  alexsubALTlem4  19738  cnextfvval  19753  snclseqg  19802  tgphaus  19803  tsmsfbas  19814  tsmssubm  19832  utopsnneip  19939  prdsxmetlem  20059  imasdsf1olem  20064  xpsdsval  20072  blres  20122  isxms2  20139  metcnp  20232  txmetcnp  20238  txmetcn  20239  metustelOLD  20242  metustel  20243  metuel2  20270  dscopn  20282  isngp4  20319  cnblcld  20470  metnrmlem1a  20550  icoopnst  20627  iocopnst  20628  elpi1  20733  lmmbr2  20886  cfil3i  20896  caucfil  20910  iscmet3  20920  lmclim  20929  metcld2  20933  bcthlem4  20954  minveclem3b  21031  minveclem6  21037  minveclem7  21038  ivthle  21056  ivthle2  21057  evthicc2  21060  ovolfioo  21067  ovolficc  21068  ovolgelb  21079  dyadmax  21194  subopnmbl  21200  ismbf3d  21248  mbfimaopnlem  21249  mbfimaopn2  21251  mbfaddlem  21254  mbfsup  21258  mbfinf  21259  i1f1lem  21283  i1fmulclem  21296  itg1climres  21308  mbfi1fseqlem4  21312  itg2monolem1  21344  itg2gt0  21354  isibl  21359  iblcnlem1  21381  ellimc2  21468  dvcnvrelem1  21605  itgsubst  21637  mdegleb  21651  fta1glem2  21754  quotval  21874  vieta1lem1  21892  vieta1lem2  21893  ulm2  21966  ulmcaulem  21975  ulmcau  21976  radcnvlt1  21999  sineq0  22099  cos11  22105  recosf1o  22107  efopn  22219  cxpeq  22311  mcubic  22358  birthdaylem3  22463  rlimcnp  22475  xrlimcnp  22478  wilth  22525  isppw  22568  isppw2  22569  mumullem2  22634  sqff1o  22636  dvdsmulf1o  22650  fsumvma  22668  fsumvma2  22669  vmasum  22671  chpchtsum  22674  lgsne0  22788  lgseisenlem2  22805  lgsquadlem1  22809  lgsquadlem2  22810  dchrmusumlema  22858  rpvmasum2  22877  dchrisum0lema  22879  pntibndlem3  22957  pntlemi  22969  pntleml  22976  pnt3  22977  trgcgrg  23086  colcom  23111  colrot1  23112  lncom  23150  mirreu3  23184  isperp  23231  perpcom  23232  brbtwn  23280  brcgr  23281  brbtwn2  23286  colinearalg  23291  axeuclidlem  23343  axcontlem2  23346  axcontlem4  23348  axcontlem7  23351  nbgraf1olem1  23485  nbgraf1olem5  23489  nbcusgra  23506  uvtx01vtx  23535  cusgrauvtxb  23539  iswlk  23561  istrl  23571  ispth  23602  isspth  23603  wlkdvspthlem  23641  usgrcyclnl2  23662  eupath2  23736  grpodiveq  23878  opidon  23944  issmgrp  23956  ismndo  23965  isrngo  24000  isdivrngo  24053  isvclem  24090  isnvlem  24123  isphg  24352  isph  24357  phoeqi  24393  ubthlem3  24408  minvecolem5  24417  minvecolem6  24418  minvecolem7  24419  hhph  24715  issh3  24757  nmopub  25447  nmfnleub  25464  adjeq  25474  adjvalval  25476  elunop2  25552  lnophm  25558  nmcexi  25565  cnlnadjlem5  25610  cnlnadjeui  25616  adjbd1o  25624  jpi  25809  mddmd2  25848  chrelati  25903  chrelat2i  25904  cvexchlem  25907  dmdbr5ati  25961  cdjreui  25971  cdj3i  25980  preqsnd  26036  disjunsn  26070  opabdm  26077  opabrn  26078  abfmpunirn  26101  feqmptdf  26112  fmptcof2  26113  ofpreima  26118  funcnvmptOLD  26120  funcnvmpt  26121  funcnv5mpt  26122  f1od2  26158  resf1o  26164  fpwrelmap  26167  negelrp  26171  iocinioc2  26203  eliccioo  26240  posrasymb  26252  isslmd  26352  pstmxmet  26458  prsdm  26478  prsrn  26479  ordtconlem1  26488  xrmulc1cn  26494  eulerpartlemmf  26892  isrrvv  26960  eldmgm  27142  dmgmaddn0  27143  lgamgulmlem6  27154  subfacp1lem3  27204  subfacp1lem6  27207  subfacp1  27208  txpcon  27255  sconpi1  27262  rescon  27269  cvmscbv  27281  cvmsval  27289  cvmlift2lem13  27338  cvmlift3lem2  27343  cvmlift3  27351  br8  27700  br6  27701  br4  27702  distel  27751  elpred  27772  poseq  27848  wsuclem  27896  sltsolem1  27943  imageval  28095  funpartfv  28110  dfrdg4  28115  altopthg  28132  altopthbg  28133  brcolinear2  28223  lineext  28241  brsegle  28273  seglelin  28281  broutsideof2  28287  onsuct0  28421  wl-sbrimt  28512  wl-sblimt  28513  wl-sbnf1  28517  wl-mo2dnae  28533  wl-mo2t  28534  wl-mo3t  28535  wl-ax11-lem6  28544  supaddc  28555  supadd  28556  tan2h  28562  ptrest  28563  mbfposadd  28577  cnambfre  28578  itg2addnclem2  28582  isfne4  28679  isfne2  28681  isfne3  28682  fneval  28697  topfneec  28701  neibastop2lem  28719  neibastop2  28720  neifg  28730  filnetlem4  28740  fdc  28779  heibor1  28847  rrncmslem  28869  rrnheibor  28874  isfldidl2  29007  isdmn3  29012  prtlem13  29151  prter3  29165  ellz1  29243  lzunuz  29244  fz1eqin  29245  diophrex  29252  rexrabdioph  29270  rexfrabdioph  29271  2rexfrabdioph  29272  3rexfrabdioph  29273  4rexfrabdioph  29274  6rexfrabdioph  29275  7rexfrabdioph  29276  fzneg  29463  expdioph  29510  wepwsolem  29532  fnwe2lem2  29542  islmodfg  29560  kercvrlsm  29574  sdrgacs  29696  pm10.52  29755  iotasbc  29811  pm14.122a  29814  pm14.122b  29815  pm14.123a  29817  rusbcALT  29831  fvsb  29846  stoweidlem34  29967  2reu4a  30151  funressnfv  30172  dfafn5a  30204  el2xptp0  30265  otthg  30268  f12dfv  30284  f13dfv  30285  elfz2z  30336  usgra2pthlem1  30438  wwlkn0s  30477  wwlkextwrd  30498  usg2spthonot  30545  isclwlk0  30557  clwwlkn2  30576  eclclwwlkn1  30644  eleclclwwlkn  30645  hashecclwwlkn1  30646  usghashecclwwlk  30647  clwlkfclwwlk1hashn  30652  clwlkfoclwwlk  30656  isrgra  30681  isrusgra  30682  wwlkextproplem3  30700  frgra3vlem2  30731  frgrancvvdeqlem2  30762  frgrancvvdeqlem3  30763  frgrancvvdeqlemC  30770  usg2spot2nb  30796  opeliun2xp  30858  fmptsnd  30860  rabssnn0fi  30885  mptnn0fsupp  30940  cply1coe0bi  30992  snlindsntor  31112  gte-lte  31355  gt-lt  31356  trsbc  31547  bnj976  32071  bnj944  32231  bnj1173  32293  bnj1321  32318  bnj1373  32321  bnj1417  32332  bj-iftru  32389  bj-iffal  32390  bj-abbi  32596  bj-tagcg  32778  bj-projval  32789  lrelat  32965  islshpat  32968  lshpsmreu  33060  lkrpssN  33114  cmtvalN  33162  omllaw2N  33195  cvrval  33220  cvrval2  33225  cvlsupr3  33295  3dim0  33407  islln2  33461  islpln5  33485  islpln2  33486  islpln2ah  33499  islvol5  33529  islvol2  33530  4atlem11  33559  pmapglbx  33719  cdleme18d  34245  cdlemefrs29bpre0  34346  cdlemb3  34556  cdlemg33b  34657  cdlemkid3N  34883  cdlemkid4  34884  dvhb1dimN  34936  dia11N  34999  cdlemm10N  35069  dib11N  35111  dib1dim  35116  dibglbN  35117  diblsmopel  35122  dihopelvalcpre  35199  dih11  35216  dihmeetlem4preN  35257  dihmeetlem13N  35270  lcfrvalsnN  35492  lcfrlem9  35501  lcf1o  35502  mapdval4N  35583  baerlem3lem2  35661  baerlem5alem2  35662  baerlem5blem2  35663  hdmap1fval  35748  hdmapfval  35781  hdmapglem7a  35881  hlhillcs  35912