Theorem syl5bb 249

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

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

This theorem is referenced by:  syl5rbb  250  syl5bbr  251  3bitr4g  280  imim21b  357  cad0  1406  had1  1408  ax11wdemo  1734  ax12olem6OLD  1982  sbcom  2138  abbi  2514  necon3abid  2600  necon3bid  2602  necon1abid  2620  r19.21t  2751  ceqsralt  2939  ceqsrexv  3029  ceqsrex2v  3031  elab2g  3044  elrabf  3051  eueq2  3068  eqreu  3086  reu8  3090  ru  3120  sbcralt  3193  csbnestgf  3259  disjpss  3638  ralprg  3817  rexprg  3818  difsn  3893  opthpr  3936  ralunsn  3963  dfiin2g  4084  iunxsng  4129  elpwuni  4138  disjxun  4170  pwnss  4325  opelopabt  4427  opelopabga  4428  brabga  4429  dfid3  4459  frirr  4519  wereu2  4539  ordtri4  4578  oneqmini  4592  elsucg  4608  elsuc2g  4609  dfwe2  4721  ssonprc  4731  ordpwsuc  4754  dfom2  4806  brab2a  4886  opeliunxp  4888  posn  4905  sosn  4906  frsn  4907  brab2ga  4910  opbrop  4914  elrnmpt1  5078  elrnmptg  5079  eliniseg2  5203  poleloe  5227  cnvpo  5369  dffun8  5439  fncnv  5474  fununi  5476  fnssresb  5516  fnimaeq0  5525  funcocnv2  5659  dffn5  5731  funimass4  5736  fnsnfv  5745  dmfco  5756  fndmdif  5793  fvimacnvi  5803  fvimacnvALT  5808  unpreima  5815  respreima  5818  fmptco  5860  fressnfv  5879  fnsuppres  5911  elunirnALT  5959  dff13  5963  fliftel  5990  isoini  6017  f1oiso  6030  f1oweALT  6033  eloprabga  6119  resoprab2  6126  ralrnmpt2  6143  ovid  6149  ov  6152  ovg  6171  ofrfval2  6282  fmpt2x  6376  ovmptss  6387  1stconst  6394  2ndconst  6395  isprmpt2  6436  brtpos2  6444  dfsmo2  6568  tfrlem1  6595  rdglim2  6649  seqomlem2  6667  omeu  6787  oeeui  6804  brdifun  6891  eqerlem  6896  brecop  6956  erovlem  6959  eceqoveq  6968  mapsn  7014  mptelixpg  7058  map1  7144  xpsnen  7151  xpdom2  7162  omxpenlem  7168  xpf1o  7228  mapunen  7235  onfin  7256  fimaxg  7313  fodomfib  7345  fofinf1o  7346  fipreima  7370  supub  7420  ordtypecbv  7442  ordtypelem3  7445  ordtypelem9  7451  hartogslem1  7467  wofib  7470  wemapso2lem  7475  wemapso2  7477  noinfep  7570  noinfepOLD  7571  cantnf  7605  rankbnd2  7751  domtri2  7832  infxpenc2  7859  fseqdom  7863  acni2  7883  dfac9  7972  cfeq0  8092  cfsuc  8093  cflim3  8098  cfslb  8102  cofsmo  8105  enfin2i  8157  isfin3ds  8165  isf33lem  8202  fin1a2lem5  8240  axdc2lem  8284  zorn2g  8339  fodomb  8360  brdom7disj  8365  brdom6disj  8366  iundom2g  8371  cfpwsdom  8415  elgch  8453  fpwwe2cbv  8461  fpwwecbv  8475  pwfseqlem3  8491  pwfseqlem4a  8492  pwfseqlem4  8493  ltpiord  8720  nlt1pi  8739  nqereu  8762  addclprlem1  8849  1idpr  8862  reclem3pr  8882  ltsosr  8925  map2psrpr  8941  supsrlem  8942  axrrecex  8994  xrlenlt  9099  eqlei2  9140  addsubeq4  9276  renegcli  9318  lesub0  9500  wloglei  9515  conjmul  9687  rereccl  9688  infm3  9923  supmul1  9929  supmullem1  9930  supmullem2  9931  supmul  9932  creui  9951  nndiv  9996  elznn0  10252  prime  10306  eqreznegel  10517  zsupss  10521  rebtwnz  10529  ltxr  10671  elixx3g  10885  ixxun  10888  ioo0  10897  ico0  10918  ioc0  10919  icc0  10920  difreicc  10984  iccf1o  10995  elfz2  11006  fzn  11027  fznn  11070  fzshftral  11089  fzosplitsni  11151  om2uzisoi  11249  sq11i  11427  hashsdom  11610  brfi1uzind  11670  wrdval  11685  s2f1o  11818  cjreb  11883  rexfiuz  12106  cau3lem  12113  rlim2  12245  ello12  12265  ello1mpt  12270  elo12  12276  o1lo1  12286  lo1resb  12313  o1resb  12315  o1compt  12336  caucvgb  12428  mertens  12618  ruclem12  12795  divides  12809  odd2np1  12863  oddm1even  12864  sadadd2lem2  12917  gcdcllem2  12967  bezoutlem2  12994  bezoutlem3  12995  bezoutlem4  12996  isprm2  13042  isprm3  13043  prmreclem2  13240  prmreclem5  13243  prmreclem6  13244  4sqlem2  13272  4sqlem12  13279  vdwmc  13301  vdwpc  13303  vdwlem6  13309  vdwlem10  13313  vdwnn  13321  ramval  13331  0ram  13343  prdsleval  13654  pwsle  13669  imasleval  13721  xpsfrnel2  13745  xpsle  13761  isacs2  13833  mreacs  13838  acsfn  13839  iscatd2  13861  catpropd  13890  isssc  13975  evlfcl  14274  uncfcurf  14291  pltval  14372  lubid  14394  tosso  14420  oduleg  14514  oduclatb  14526  isipodrs  14542  odudlatb  14577  spwpr2  14615  spwex  14616  gsumvalx  14729  grplmulf1o  14820  grplactcnv  14842  elnmz  14934  eqgid  14947  isghm  14961  ghmeqker  14987  resscntz  15085  odmulgeq  15148  sylow3lem3  15218  sylow3lem6  15221  efgval2  15311  efgsdm  15317  efgrelexlema  15336  efgcpbllemb  15342  iscyggen2  15446  cyggenod  15449  eldprd  15517  dprdf11  15536  dprddisj2  15552  pgpfac1lem2  15588  pgpfac1  15593  drngid2  15806  issubrg  15823  islmod  15909  aspval2  16360  psrbag  16386  zndvds  16785  znleval  16790  iunocv  16863  pjfval2  16891  pjdm2  16893  istopg  16923  istpsOLD  16940  basgen2  17009  isclo  17106  mretopd  17111  isnei  17122  isperf3  17171  restdis  17196  neitr  17198  restcls  17199  restlp  17201  restperf  17202  iscn  17253  iscnp  17255  lmbr2  17277  lmbrf  17278  ordtt1  17397  cmpsub  17417  hauscmplem  17423  cmpfi  17425  dfcon2  17435  1stcelcls  17477  1stccn  17479  nllyi  17491  subislly  17497  elkgen  17521  ptpjpre1  17556  ptuni2  17561  ptclsg  17600  ptcnplem  17606  txcn  17611  hausdiag  17630  txhaus  17632  txkgen  17637  xkoptsub  17639  cnmpt21  17656  elqtop  17682  tgqtop  17697  r0cld  17723  elfg  17856  fbasrn  17869  trfil2  17872  trfil3  17873  fin1aufil  17917  elfm2  17933  elfm3  17935  flimopn  17960  fbflim  17961  flfnei  17976  flftg  17981  cnpflf2  17985  txflf  17991  fclsbas  18006  alexsubALTlem4  18034  cnextfvval  18049  snclseqg  18098  tgphaus  18099  tsmsfbas  18110  tsmssubm  18125  utopsnneip  18231  prdsxmetlem  18351  imasdsf1olem  18356  xpsdsval  18364  blres  18414  isxms2  18431  metcnp  18524  txmetcnp  18530  txmetcn  18531  metustelOLD  18534  metustel  18535  metuel2  18562  dscopn  18574  isngp4  18611  cnblcld  18762  metnrmlem1a  18841  icoopnst  18917  iocopnst  18918  elpi1  19023  lmmbr2  19165  cfil3i  19175  caucfil  19189  iscmet3  19199  lmclim  19208  metcld2  19212  bcthlem4  19233  minveclem3b  19282  minveclem6  19288  minveclem7  19289  ivthle  19306  ivthle2  19307  evthicc2  19310  ovolfioo  19317  ovolficc  19318  ovolgelb  19329  dyadmax  19443  subopnmbl  19449  ismbf3d  19499  mbfimaopnlem  19500  mbfimaopn2  19502  mbfaddlem  19505  mbfsup  19509  mbfinf  19510  i1f1lem  19534  i1fmulclem  19547  itg1climres  19559  mbfi1fseqlem4  19563  itg2monolem1  19595  itg2gt0  19605  isibl  19610  iblcnlem1  19632  ellimc2  19717  dvcnvrelem1  19854  itgsubst  19886  mdegleb  19940  fta1glem2  20042  quotval  20162  vieta1lem1  20180  vieta1lem2  20181  ulm2  20254  ulmcaulem  20263  ulmcau  20264  radcnvlt1  20287  sineq0  20382  cos11  20388  recosf1o  20390  efopn  20502  cxpeq  20594  mcubic  20640  birthdaylem3  20745  rlimcnp  20757  xrlimcnp  20760  wilth  20807  isppw  20850  isppw2  20851  mumullem2  20916  sqff1o  20918  dvdsmulf1o  20932  fsumvma  20950  fsumvma2  20951  vmasum  20953  chpchtsum  20956  lgsne0  21070  lgseisenlem2  21087  lgsquadlem1  21091  lgsquadlem2  21092  dchrmusumlema  21140  rpvmasum2  21159  dchrisum0lema  21161  pntibndlem3  21239  pntlemi  21251  pntleml  21258  pnt3  21259  nbgraf1olem1  21404  nbgraf1olem5  21408  nbcusgra  21425  uvtx01vtx  21454  cusgrauvtxb  21458  iswlk  21480  istrl  21490  ispth  21521  isspth  21522  wlkdvspthlem  21560  usgrcyclnl2  21581  eupath2  21655  grpodiveq  21797  opidon  21863  issmgrp  21875  ismndo  21884  isrngo  21919  isdivrngo  21972  isvclem  22009  isnvlem  22042  isphg  22271  isph  22276  phoeqi  22312  ubthlem3  22327  minvecolem5  22336  minvecolem6  22337  minvecolem7  22338  hhph  22633  issh3  22675  nmopub  23364  nmfnleub  23381  adjeq  23391  adjvalval  23393  elunop2  23469  lnophm  23475  nmcexi  23482  cnlnadjlem5  23527  cnlnadjeui  23533  adjbd1o  23541  jpi  23726  mddmd2  23765  chrelati  23820  chrelat2i  23821  cvexchlem  23824  dmdbr5ati  23878  cdjreui  23888  cdj3i  23897  preqsnd  23953  abfmpunirn  24017  feqmptdf  24028  fmptcof2  24029  ofpreima  24034  funcnvmptOLD  24035  funcnvmpt  24036  funcnv5mpt  24037  iocinioc2  24095  eliccioo  24130  pstmxmet  24245  xrmulc1cn  24269  isrrvv  24654  eldmgm  24759  dmgmaddn0  24760  lgamgulmlem6  24771  subfacp1lem3  24821  subfacp1lem6  24824  subfacp1  24825  txpcon  24872  sconpi1  24879  rescon  24886  cvmscbv  24898  cvmsval  24906  cvmlift2lem13  24955  cvmlift3lem2  24960  cvmlift3  24968  divelunit  25138  br8  25327  br6  25328  br4  25329  distel  25374  elpred  25391  poseq  25467  sltsolem1  25536  elfuns  25668  imageval  25683  funpartfv  25698  dfrdg4  25703  altopthg  25716  altopthbg  25717  brbtwn  25742  brcgr  25743  brbtwn2  25748  colinearalg  25753  axeuclidlem  25805  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  brcolinear2  25896  lineext  25914  brsegle  25946  seglelin  25954  broutsideof2  25960  bpolyval  25999  onsuct0  26095  supaddc  26137  supadd  26138  mbfposadd  26153  cnambfre  26154  itg2addnclem2  26156  isfne4  26239  isfne2  26241  isfne3  26242  fneval  26257  topfneec  26261  neibastop2lem  26279  neibastop2  26280  neifg  26290  filnetlem4  26300  fdc  26339  heibor1  26409  rrncmslem  26431  rrnheibor  26436  isfldidl2  26569  isdmn3  26574  prtlem13  26607  prter3  26621  fnnfpeq0  26629  ralxpxfr2d  26631  ellz1  26715  lzunuz  26716  fz1eqin  26717  diophrex  26724  rexrabdioph  26744  rexfrabdioph  26745  2rexfrabdioph  26746  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  fzneg  26937  expdioph  26984  wepwsolem  27006  fnwe2lem2  27016  islmodfg  27035  kercvrlsm  27049  dsmmelbas  27073  ellspd  27122  islindf  27150  islindf4  27176  f1omvdconj  27257  sdrgacs  27377  pm10.52  27428  iotasbc  27487  pm14.122a  27490  pm14.122b  27491  pm14.123a  27493  rusbcALT  27507  fvsb  27522  stoweidlem34  27650  2reu4a  27834  sbcfun  27854  funressnfv  27859  dfafn5a  27891  el2xptp0  27949  otthg  27952  f12dfv  27961  f13dfv  27962  euhash1  27998  usgra2pthlem1  28040  usg2spthonot  28085  frgra3vlem2  28105  frgrancvvdeqlem2  28134  frgrancvvdeqlem3  28135  frgrancvvdeqlemC  28142  usg2spot2nb  28168  gte-lte  28181  gt-lt  28182  bnj976  28854  bnj944  29015  bnj1173  29077  bnj1321  29102  bnj1373  29105  bnj1417  29116  ax12olem6NEW7  29165  sbcomwAUX7  29291  sbcomOLD7  29439  lrelat  29497  islshpat  29500  lshpsmreu  29592  lkrpssN  29646  cmtvalN  29694  omllaw2N  29727  cvrval  29752  cvrval2  29757  cvlsupr3  29827  3dim0  29939  islln2  29993  islpln5  30017  islpln2  30018  islpln2ah  30031  islvol5  30061  islvol2  30062  4atlem11  30091  pmapglbx  30251  cdleme18d  30777  cdlemefrs29bpre0  30878  cdlemb3  31088  cdlemg33b  31189  dvhb1dimN  31468  dia11N  31531  cdlemm10N  31601  dib11N  31643  dib1dim  31648  dibglbN  31649  diblsmopel  31654  dihopelvalcpre  31731  dih11  31748  dihmeetlem4preN  31789  dihmeetlem13N  31802  lcfrvalsnN  32024  lcfrlem9  32033  lcf1o  32034  mapdval4N  32115  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  hdmap1fval  32280  hdmapfval  32313  hdmapglem7a  32413  hlhillcs  32444

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178