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  1513  ax12wdemo  1885  sbal2  2262  necon3abid  2632  necon3bid  2640  r19.21tOLD  2758  ceqsralt  3042  ralxpxfr2d  3134  ceqsrexv  3142  ceqsrex2v  3144  elab2g  3157  elrabf  3164  elrab3t  3165  eueq2  3182  eqreu  3200  reu8  3204  ru  3236  sbcralt  3310  sbcabel  3315  sbcel1g  3744  sbcel2  3746  csbnestgf  3753  sbccsb2  3762  disjpss  3783  sbcssg  3848  rexsng  3973  ralprg  3987  rexprg  3988  difsn  4072  opthpr  4116  ralunsn  4145  csbuni  4185  dfiin2g  4270  iunxsng  4319  elpwuni  4328  disjxun  4359  sbcbr12g  4415  pwnss  4527  opthneg  4638  otthg  4642  opelopabt  4670  opelopabga  4671  brabga  4672  csbmpt12  4692  dfid3  4707  frirr  4768  wereu2  4788  brab2a  4841  opeliunxp  4843  posn  4860  sosn  4861  frsn  4862  brab2ga  4867  opbrop  4871  csbcnvgALT  4976  elrnmpt1  5040  elrnmptg  5041  eliniseg2  5166  poleloe  5188  xpdifid  5222  cnvpo  5331  elpred  5350  ordtri4  5417  oneqmini  5431  elsucg  5447  elsuc2g  5448  sbcfung  5562  dffun8  5566  fncnv  5603  fununi  5605  fnssresb  5644  fnimaeq0  5653  funcocnv2  5793  csbfv12  5855  dffn5  5865  funimass4  5871  fnsnfv  5880  dmfco  5894  fndmdif  5940  fvimacnvi  5950  fvimacnvALT  5955  unpreima  5960  respreima  5963  fmptco  6010  fressnfv  6032  fmptsnd  6040  fnnfpeq0  6049  tpres  6071  elunirn  6110  dff13  6113  f12dfv  6126  f13dfv  6127  fliftel  6156  isoini  6183  f1oiso  6196  eloprabga  6336  resoprab2  6346  elrnmpt2res  6363  ralrnmpt2  6364  ovid  6366  ov  6369  ovg  6388  ofrfval2  6502  dfwe2  6561  ssonprc  6572  ordpwsuc  6595  dfom2  6647  f1oweALT  6730  el2xptp0  6790  fmpt2x  6812  ovmptss  6827  1stconst  6834  2ndconst  6835  fnsuppres  6892  isprmpt2  6921  brtpos2  6929  mpt2curryd  6966  dfsmo2  7016  rdglim2  7100  seqomlem2  7118  omeu  7236  oeeui  7253  brdifun  7340  eqerlem  7345  brecop  7406  erovlem  7409  eceqoveq  7418  mapsn  7463  ixpsnval  7475  mptelixpg  7509  map1  7597  xpsnen  7604  xpdom2  7615  omxpenlem  7621  xpf1o  7682  mapunen  7689  onfin  7711  fimaxg  7766  fodomfib  7799  fofinf1o  7800  fipreima  7828  supub  7921  infglb  7954  infglbb  7955  fiming  7962  fiinfg  7963  ordtypecbv  7980  ordtypelem3  7983  ordtypelem9  7989  hartogslem1  8005  wofib  8008  wemapsolem  8013  wemapso2lem  8015  noinfep  8112  cantnf  8145  rankbnd2  8287  domtri2  8370  infxpenc2  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  8993  fpwwe2cbv  9001  fpwwecbv  9015  pwfseqlem3  9031  pwfseqlem4a  9032  pwfseqlem4  9033  ltpiord  9258  nlt1pi  9277  nqereu  9300  addclprlem1  9387  1idpr  9400  reclem3pr  9420  ltsosr  9464  map2psrpr  9480  supsrlem  9481  axrrecex  9533  xrlenlt  9645  eqlei2  9691  addsubeq4  9836  renegcli  9881  lesub0  10077  wloglei  10092  conjmul  10270  rereccl  10271  infm3  10514  supaddc  10520  supadd  10521  supmul1  10522  supmullem1  10523  supmullem2  10524  supmul  10525  creui  10550  nndiv  10596  elznn0  10898  prime  10962  eqreznegel  11195  zsupss  11199  rebtwnz  11209  negelrp  11279  ltxr  11361  elixx3g  11594  ixxun  11597  ioo0  11607  ico0  11628  ioc0  11629  icc0  11630  difreicc  11710  divelunit  11720  iccf1o  11722  elfz2  11737  fzn  11761  fznn  11809  fzshftral  11828  nelfzo  11871  fzosplitsni  11964  om2uzisoi  12113  rabssnn0fi  12143  mptnn0fsupp  12154  sq11i  12310  hashsdom  12505  fi1uzind  12593  wrdval  12617  csbwrdg  12639  wrd2ind  12775  s2f1o  12940  cjreb  13125  rexfiuz  13349  cau3lem  13356  rlim2  13498  ello12  13518  ello1mpt  13523  elo12  13529  o1lo1  13539  lo1resb  13566  o1resb  13568  o1compt  13589  caucvgb  13684  mertens  13880  ruclem12  14231  divides  14245  odd2np1  14303  oddm1even  14304  sadadd2lem2  14362  gcdcllem2  14412  bezoutlem2OLD  14442  bezoutlem3OLD  14443  bezoutlem4OLD  14444  bezoutlem2  14445  bezoutlem3  14446  bezoutlem4  14447  isprm2  14570  isprm3  14571  prmreclem2  14799  prmreclem5  14802  prmreclem6  14803  4sqlem2  14831  4sqlem12  14838  vdwmc  14866  vdwpc  14868  vdwlem6  14874  vdwlem10  14878  vdwnn  14886  ramval  14898  ramvalOLD  14899  0ram  14916  prdsleval  15313  pwsle  15328  imasleval  15385  xpsfrnel2  15409  xpsle  15425  isacs2  15497  mreacs  15502  acsfn  15503  iscatd2  15525  catpropd  15552  ciclcl  15645  cicrcl  15646  isssc  15663  evlfcl  16045  uncfcurf  16062  pltval  16144  lublecllem  16172  tosso  16220  oduleg  16316  oduclatb  16328  posglbmo  16331  isipodrs  16345  odudlatb  16380  gsumvalx  16451  sgrp2rid2  16598  grplmulf1o  16666  grplactcnv  16692  elnmz  16794  eqgid  16807  isghm  16821  ghmeqker  16847  resscntz  16923  symg1bas  16975  pgrpsubgsymgbi  16986  symgfixelq  17012  f1omvdconj  17025  odmulgeq  17146  sylow3lem3  17219  sylow3lem6  17222  efgval2  17312  efgsdm  17318  efgrelexlema  17337  efgcpbllemb  17343  iscyggen2  17454  cyggenod  17457  gsummptfzcl  17539  eldprd  17574  dprdf11  17594  dprddisj2  17610  pgpfac1lem2  17646  pgpfac1  17651  srg1zr  17700  drngid2  17929  issubrg  17946  islmod  18033  aspval2  18509  psrbag  18526  cply1coe0bi  18832  zndvds  19057  znleval  19062  iunocv  19181  pjfval2  19209  pjdm2  19211  dsmmelbas  19239  ellspd  19297  islindf  19307  islindf4  19333  istopg  19862  basgen2  19942  isclo  20040  mretopd  20045  isnei  20056  isperf3  20106  restdis  20131  neitr  20133  restcls  20134  restlp  20136  restperf  20137  iscn  20188  iscnp  20190  lmbr2  20212  lmbrf  20213  ordtt1  20332  cmpsub  20352  hauscmplem  20358  cmpfi  20360  dfcon2  20371  1stcelcls  20413  1stccn  20415  nllyi  20427  subislly  20433  dissnlocfin  20481  elkgen  20488  ptpjpre1  20523  ptuni2  20528  ptclsg  20567  ptcnplem  20573  txcn  20578  hausdiag  20597  txhaus  20599  txkgen  20604  xkoptsub  20606  cnmpt21  20623  elqtop  20649  tgqtop  20664  r0cld  20690  elfg  20823  fbasrn  20836  trfil2  20839  trfil3  20840  fin1aufil  20884  elfm2  20900  elfm3  20902  flimopn  20927  fbflim  20928  flfnei  20943  flftg  20948  cnpflf2  20952  txflf  20958  fclsbas  20973  alexsubALTlem4  21002  cnextfvval  21017  snclseqg  21067  tgphaus  21068  tsmsfbas  21079  tsmssubm  21094  utopsnneip  21200  prdsxmetlem  21320  imasdsf1olem  21325  xpsdsval  21333  blres  21383  isxms2  21400  metcnp  21493  txmetcnp  21499  txmetcn  21500  metustel  21502  metuel2  21517  dscopn  21525  isngp4  21562  cnblcld  21732  metnrmlem1a  21812  metnrmlem1aOLD  21827  icoopnst  21904  iocopnst  21905  elpi1  22013  lmmbr2  22166  cfil3i  22176  caucfil  22190  iscmet3  22200  lmclim  22209  metcld2  22213  bcthlem4  22232  minveclem3b  22307  minveclem6  22313  minveclem7  22314  minveclem3bOLD  22319  minveclem6OLD  22325  minveclem7OLD  22326  ivthle  22344  ivthle2  22345  evthicc2  22348  ovolfioo  22357  ovolficc  22358  ovolgelb  22370  dyadmax  22493  subopnmbl  22499  ismbf3d  22547  mbfimaopnlem  22548  mbfimaopn2  22550  mbfaddlem  22553  mbfsup  22557  mbfinf  22558  mbfinfOLD  22559  i1f1lem  22584  i1fmulclem  22597  itg1climres  22609  mbfi1fseqlem4  22613  itg2monolem1  22645  itg2gt0  22655  isibl  22660  iblcnlem1  22682  ellimc2  22769  dvcnvrelem1  22906  itgsubst  22938  mdegleb  22950  fta1glem2  23054  quotval  23182  vieta1lem1  23200  vieta1lem2  23201  ulm2  23277  ulmcaulem  23286  ulmcau  23287  radcnvlt1  23310  sineq0  23413  cos11  23419  recosf1o  23421  efopn  23540  cxpeq  23634  mcubic  23710  birthdaylem3  23816  rlimcnp  23828  xrlimcnp  23831  eldmgm  23884  dmgmaddn0  23885  lgamgulmlem6  23896  wilth  23933  isppw  23978  isppw2  23979  mumullem2  24044  sqff1o  24046  dvdsmulf1o  24060  fsumvma  24078  fsumvma2  24079  vmasum  24081  chpchtsum  24084  lgsne0  24198  lgseisenlem2  24215  lgsquadlem1  24219  lgsquadlem2  24220  dchrmusumlema  24268  rpvmasum2  24287  dchrisum0lema  24289  pntibndlem3  24367  pntlemi  24379  pntleml  24386  pnt3  24387  trgcgrg  24497  tgcgr4  24513  colcom  24540  colrot1  24541  ltgov  24579  hlcomb  24585  lncom  24604  mirreu3  24636  isperp  24694  perpcom  24695  brbtwn  24866  brcgr  24867  brbtwn2  24872  colinearalg  24877  axeuclidlem  24929  axcontlem2  24932  axcontlem4  24934  axcontlem7  24937  nbgraf1olem1  25106  nbgraf1olem5  25110  nbcusgra  25128  uvtx01vtx  25157  cusgrauvtxb  25161  iswlk  25185  istrl  25204  ispth  25235  isspth  25236  wlkdvspthlem  25274  usgrcyclnl2  25306  wwlkn0s  25370  wwlkextwrd  25393  wwlkextproplem3  25408  isclwlk0  25419  clwwlkn2  25440  eclclwwlkn1  25497  eleclclwwlkn  25498  hashecclwwlkn1  25499  usghashecclwwlk  25500  clwlkfclwwlk1hashn  25506  clwlkfoclwwlk  25510  usg2spthonot  25553  isrgra  25591  isrusgra  25592  isrusgusrg  25597  eupath2  25645  frgra3vlem2  25666  frgrancvvdeqlem2  25696  frgrancvvdeqlem3  25697  frgrancvvdeqlemC  25704  usg2spot2nb  25730  grpodiveq  25921  opidonOLD  25987  issmgrpOLD  25999  ismndo  26008  isrngo  26043  isdivrngo  26096  isvclem  26133  isnvlem  26166  isphg  26395  isph  26400  phoeqi  26436  ubthlem3  26451  minvecolem5  26460  minvecolem6  26461  minvecolem7  26462  minvecolem5OLD  26470  minvecolem6OLD  26471  minvecolem7OLD  26472  hhph  26768  issh3  26809  nmopub  27498  nmfnleub  27515  adjeq  27525  adjvalval  27527  elunop2  27603  lnophm  27609  nmcexi  27616  cnlnadjlem5  27661  cnlnadjeui  27667  adjbd1o  27675  jpi  27860  mddmd2  27899  chrelati  27954  chrelat2i  27955  cvexchlem  27958  dmdbr5ati  28012  cdjreui  28022  cdj3i  28031  preqsnd  28098  iunxsngf  28113  disjunsn  28145  opeldifid  28151  fcoinvbr  28156  brabgaf  28157  opabdm  28160  opabrn  28161  iunsnima  28165  abfmpunirn  28192  feqmptdf  28199  fmptcof2  28200  funcnvmptOLD  28211  funcnvmpt  28212  funcnv5mpt  28213  f1od2  28254  resf1o  28260  fpwrelmap  28263  iocinioc2  28306  eliccioo  28346  posrasymb  28364  isslmd  28464  smatrcl  28569  pstmxmet  28647  prsdm  28667  prsrn  28668  ordtconlem1  28677  xrmulc1cn  28683  ispisys2  28922  elcarsg  29084  eulerpartlemmf  29155  isrrvv  29223  bnj976  29536  bnj944  29696  bnj1173  29758  bnj1321  29783  bnj1373  29786  bnj1417  29797  subfacp1lem3  29852  subfacp1lem6  29855  subfacp1  29856  txpcon  29902  sconpi1  29909  rescon  29916  cvmscbv  29928  cvmsval  29936  cvmlift2lem13  29985  cvmlift3lem2  29990  cvmlift3  29998  mclsrcl  30146  br8  30342  br6  30343  br4  30344  fv1stcnv  30368  fv2ndcnv  30369  distel  30396  poseq  30437  wsuclem  30454  sltsolem1  30501  imageval  30641  funpartfv  30656  dfrdg4  30662  altopthg  30678  altopthbg  30679  brcolinear2  30769  lineext  30787  brsegle  30819  seglelin  30827  broutsideof2  30833  isfne4  30940  isfne2  30942  isfne3  30943  fneval  30952  topfneec  30955  neibastop2lem  30960  neibastop2  30961  neifg  30971  filnetlem4  30981  onsuct0  31045  bj-abbi  31301  bj-tagcg  31490  bj-projval  31501  csbopg2  31632  csbwrecsg  31635  csboprabg  31638  csbmpt22g  31639  topdifinffinlem  31657  isbasisrelowllem1  31665  isbasisrelowllem2  31666  rdgeqoa  31680  csbfinxpg  31687  wl-sbrimt  31785  wl-sblimt  31786  wl-sbnf1  31790  wl-mo2df  31806  wl-eudf  31808  wl-mo2t  31811  wl-mo3t  31812  wl-ax11-lem6  31827  tan2h  31844  ptrest  31846  poimirlem2  31849  poimirlem16  31863  poimirlem19  31866  poimirlem23  31870  poimirlem24  31871  poimirlem25  31872  poimirlem26  31873  poimirlem27  31874  mbfposadd  31895  cnambfre  31896  itg2addnclem2  31901  fdc  31981  heibor1  32049  rrncmslem  32071  rrnheibor  32076  isfldidl2  32209  isdmn3  32214  prtlem13  32351  prter3  32365  lrelat  32492  islshpat  32495  lshpsmreu  32587  lkrpssN  32641  cmtvalN  32689  omllaw2N  32722  cvrval  32747  cvrval2  32752  cvlsupr3  32822  3dim0  32934  islln2  32988  islpln5  33012  islpln2  33013  islpln2ah  33026  islvol5  33056  islvol2  33057  4atlem11  33086  pmapglbx  33246  cdleme18d  33773  cdlemefrs29bpre0  33875  cdlemb3  34085  cdlemg33b  34186  cdlemkid3N  34412  cdlemkid4  34413  dvhb1dimN  34465  dia11N  34528  cdlemm10N  34598  dib11N  34640  dib1dim  34645  dibglbN  34646  diblsmopel  34651  dihopelvalcpre  34728  dih11  34745  dihmeetlem4preN  34786  dihmeetlem13N  34799  lcfrvalsnN  35021  lcfrlem9  35030  lcf1o  35031  mapdval4N  35112  baerlem3lem2  35190  baerlem5alem2  35191  baerlem5blem2  35192  hdmap1fval  35277  hdmapfval  35310  hdmapglem7a  35410  hlhillcs  35441  ellz1  35521  lzunuz  35522  fz1eqin  35523  diophrex  35530  rexrabdioph  35549  rexfrabdioph  35550  2rexfrabdioph  35551  3rexfrabdioph  35552  4rexfrabdioph  35553  6rexfrabdioph  35554  7rexfrabdioph  35555  fzneg  35745  expdioph  35791  wepwsolem  35813  fnwe2lem2  35822  islmodfg  35840  kercvrlsm  35854  sdrgacs  35980  cnvcnvintabd  36119  iunrelexpuztr  36224  brtrclfv2  36232  frege124d  36266  pm10.52  36627  iotasbc  36683  pm14.122a  36686  pm14.122b  36687  pm14.123a  36689  rusbcALT  36703  fvsb  36718  trsbc  36814  rexsngf  37307  iunxsngf2  37318  limcperiod  37591  limsupre  37604  limsupreOLD  37605  dvbdfbdioo  37685  stoweidlem34  37778  fourierdlem108  37961  fourierdlem110  37963  etransc  38032  2reu4a  38424  funressnfv  38443  dfafn5a  38475  el1fzopredsuc  38535  iccelpart  38560  dfeven2  38592  gboge7  38677  bgoldbwt  38691  elfz2z  38852  isuhgr  38925  isushgr  38926  isupgr  38950  isumgr  38959  isuspgr  38998  isusgr  38999  uhgr0v0e  39059  isfusgrf1  39123  opfusgr  39125  usgr1v0e  39128  nbuhgr2vtx1edgb  39156  edgnbusgreu  39177  nbusgredgeu0  39178  isuvtxa  39197  cusgruvtxb  39218  cplgr3v  39230  cusgrsizeinds  39241  usgra2pthlem1  39258  isuhgrALTV  39269  isushgrALTV  39270  usgo0s0ALT  39339  usgo1s0ALT  39340  ismhm0  39396  inclfusubc  39458  isrnghm  39483  rnghmval2  39486  uzlidlring  39520  lidldomnnring  39521  zrninitoringc  39664  opeliun2xp  39707  snlindsntor  39857  elbigo2  39956  gte-lte  40037  gt-lt  40038