MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5bb Unicode version

Theorem syl5bb 248
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
StepHypRef Expression
1 syl5bb.1 . . 3  |-  ( ph  <->  ps )
21a1i 10 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
3 syl5bb.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3bitrd 244 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  syl5rbb  249  syl5bbr  250  3bitr4g  279  imim21b  356  cad0  1390  had1  1392  ax11wdemo  1697  ax12olem6  1873  sbcom  2029  abbi  2393  necon3abid  2479  necon3bid  2481  necon1abid  2499  r19.21t  2628  ceqsralt  2811  ceqsrexv  2901  ceqsrex2v  2903  elab2g  2916  elrabf  2922  eueq2  2939  eqreu  2957  reu8  2961  ru  2990  sbcralt  3063  sbcabel  3068  csbnestgf  3129  disjpss  3505  ralprg  3682  rexprg  3683  difsn  3755  opthpr  3790  ralunsn  3815  dfiin2g  3936  iunxsng  3980  elpwuni  3989  disjxun  4021  pwnss  4176  opelopabt  4277  opelopabga  4278  brabga  4279  dfid3  4310  frirr  4370  wereu2  4390  ordtri4  4429  oneqmini  4443  elsucg  4459  elsuc2g  4460  dfwe2  4573  ssonprc  4583  ordpwsuc  4606  dfom2  4658  brab2a  4738  opeliunxp  4740  posn  4758  sosn  4759  frsn  4760  brab2ga  4763  opbrop  4767  elrnmpt1  4928  elrnmptg  4929  eliniseg2  5053  poleloe  5077  cnvpo  5213  dffun8  5281  fncnv  5314  fununi  5316  fnssresb  5356  fnimaeq0  5365  funcocnv2  5498  dffn5  5568  funimass4  5573  fnsnfv  5582  dmfco  5593  fndmdif  5629  fvimacnvi  5639  fvimacnvALT  5644  unpreima  5651  respreima  5654  fmptco  5691  fressnfv  5707  fnsuppres  5732  elunirnALT  5779  dff13  5783  fliftel  5808  isoini  5835  f1oiso  5848  f1oweALT  5851  eloprabga  5934  resoprab2  5941  ralrnmpt2  5958  ovid  5964  ov  5967  ovg  5986  ofrfval2  6096  fmpt2x  6190  ovmptss  6200  1stconst  6207  2ndconst  6208  brtpos2  6240  dfsmo2  6364  tfrlem1  6391  rdglim2  6445  seqomlem2  6463  omeu  6583  oeeui  6600  brdifun  6687  eqerlem  6692  brecop  6751  erovlem  6754  eceqoveq  6763  mapsn  6809  mptelixpg  6853  map1  6939  xpsnen  6946  xpdom2  6957  omxpenlem  6963  xpf1o  7023  mapunen  7030  onfin  7051  fimaxg  7104  fodomfib  7136  fofinf1o  7137  fipreima  7161  supub  7210  ordtypecbv  7232  ordtypelem3  7235  ordtypelem9  7241  hartogslem1  7257  wofib  7260  wemapso2lem  7265  wemapso2  7267  noinfep  7360  noinfepOLD  7361  cantnf  7395  rankbnd2  7541  domtri2  7622  infxpenc2  7649  fseqdom  7653  acni2  7673  dfac9  7762  cfeq0  7882  cfsuc  7883  cflim3  7888  cfslb  7892  cofsmo  7895  enfin2i  7947  isfin3ds  7955  isf33lem  7992  fin1a2lem5  8030  axdc2lem  8074  zorn2g  8130  fodomb  8151  brdom7disj  8156  brdom6disj  8157  iundom2g  8162  cfpwsdom  8206  elgch  8244  fpwwe2cbv  8252  fpwwecbv  8266  pwfseqlem3  8282  pwfseqlem4a  8283  pwfseqlem4  8284  ltpiord  8511  nlt1pi  8530  nqereu  8553  addclprlem1  8640  1idpr  8653  reclem3pr  8673  ltsosr  8716  map2psrpr  8732  supsrlem  8733  axrrecex  8785  xrlenlt  8890  addsubeq4  9066  renegcli  9108  lesub0  9290  wloglei  9305  conjmul  9477  rereccl  9478  infm3  9713  supmul1  9719  supmullem1  9720  supmullem2  9721  supmul  9722  creui  9741  nndiv  9786  elznn0  10038  prime  10092  eqreznegel  10303  zsupss  10307  rebtwnz  10315  ltxr  10457  elixx3g  10669  ixxun  10672  ioo0  10681  ico0  10702  ioc0  10703  icc0  10704  difreicc  10767  iccf1o  10778  elfz2  10789  fzn  10810  fznn  10852  fzshftral  10869  fzosplitsni  10921  om2uzisoi  11017  sq11i  11194  hashsdom  11363  wrdval  11416  cjreb  11608  rexfiuz  11831  cau3lem  11838  rlim2  11970  ello12  11990  ello1mpt  11995  elo12  12001  o1lo1  12011  lo1resb  12038  o1resb  12040  o1compt  12061  caucvgb  12152  mertens  12342  ruclem12  12519  divides  12533  odd2np1  12587  oddm1even  12588  sadadd2lem2  12641  gcdcllem2  12691  bezoutlem2  12718  bezoutlem3  12719  bezoutlem4  12720  isprm2  12766  isprm3  12767  prmreclem2  12964  prmreclem5  12967  prmreclem6  12968  4sqlem2  12996  4sqlem12  13003  vdwmc  13025  vdwpc  13027  vdwlem6  13033  vdwlem10  13037  vdwnn  13045  ramval  13055  0ram  13067  prdsleval  13376  pwsle  13391  imasleval  13443  xpsfrnel2  13467  xpsle  13483  isacs2  13555  mreacs  13560  acsfn  13561  iscatd2  13583  catpropd  13612  isssc  13697  evlfcl  13996  uncfcurf  14013  pltval  14094  lubid  14116  tosso  14142  oduleg  14236  oduclatb  14248  isipodrs  14264  odudlatb  14299  spwpr2  14337  spwex  14338  gsumvalx  14451  grplmulf1o  14542  grplactcnv  14564  elnmz  14656  eqgid  14669  isghm  14683  ghmeqker  14709  resscntz  14807  odmulgeq  14870  sylow3lem3  14940  sylow3lem6  14943  efgval2  15033  efgsdm  15039  efgrelexlema  15058  efgcpbllemb  15064  iscyggen2  15168  cyggenod  15171  eldprd  15239  dprdf11  15258  dprddisj2  15274  pgpfac1lem2  15310  pgpfac1  15315  drngid2  15528  issubrg  15545  islmod  15631  aspval2  16086  psrbag  16112  zndvds  16503  znleval  16508  iunocv  16581  pjfval2  16609  pjdm2  16611  istopg  16641  istpsOLD  16658  basgen2  16727  isclo  16824  mretopd  16829  isnei  16840  isperf3  16884  restdis  16909  restcls  16911  restlp  16913  restperf  16914  iscn  16965  iscnp  16967  lmbr2  16989  lmbrf  16990  ordtt1  17107  cmpsub  17127  hauscmplem  17133  cmpfi  17135  dfcon2  17145  1stcelcls  17187  1stccn  17189  nllyi  17201  subislly  17207  elkgen  17231  ptpjpre1  17266  ptuni2  17271  ptclsg  17309  ptcnplem  17315  txcn  17320  hausdiag  17339  txhaus  17341  txkgen  17346  xkoptsub  17348  cnmpt21  17365  elqtop  17388  tgqtop  17403  r0cld  17429  elfg  17566  fbasrn  17579  trfil2  17582  trfil3  17583  fin1aufil  17627  elfm2  17643  elfm3  17645  flimopn  17670  fbflim  17671  flfnei  17686  flftg  17691  cnpflf2  17695  txflf  17701  fclsbas  17716  alexsubALTlem4  17744  snclseqg  17798  tgphaus  17799  tsmsfbas  17810  tsmssubm  17825  prdsxmetlem  17932  imasdsf1olem  17937  xpsdsval  17945  blres  17977  isxms2  17994  metcnp  18087  txmetcnp  18093  txmetcn  18094  dscopn  18096  isngp4  18133  cnblcld  18284  metnrmlem1a  18362  icoopnst  18437  iocopnst  18438  elpi1  18543  lmmbr2  18685  cfil3i  18695  caucfil  18709  iscmet3  18719  lmclim  18728  metcld2  18732  bcthlem4  18749  minveclem3b  18792  minveclem6  18798  minveclem7  18799  ivthle  18816  ivthle2  18817  evthicc2  18820  ovolfioo  18827  ovolficc  18828  ovolgelb  18839  dyadmax  18953  subopnmbl  18959  ismbf3d  19009  mbfimaopnlem  19010  mbfimaopn2  19012  mbfaddlem  19015  mbfsup  19019  mbfinf  19020  i1f1lem  19044  i1fmulclem  19057  itg1climres  19069  mbfi1fseqlem4  19073  itg2monolem1  19105  itg2gt0  19115  isibl  19120  iblcnlem1  19142  ellimc2  19227  dvcnvrelem1  19364  itgsubst  19396  mdegleb  19450  fta1glem2  19552  quotval  19672  vieta1lem1  19690  vieta1lem2  19691  ulm2  19764  ulmcaulem  19771  ulmcau  19772  radcnvlt1  19794  sineq0  19889  cos11  19895  recosf1o  19897  efopn  20005  cxpeq  20097  mcubic  20143  birthdaylem3  20248  rlimcnp  20260  xrlimcnp  20263  wilth  20309  isppw  20352  isppw2  20353  mumullem2  20418  sqff1o  20420  dvdsmulf1o  20434  fsumvma  20452  fsumvma2  20453  vmasum  20455  chpchtsum  20458  lgsne0  20572  lgseisenlem2  20589  lgsquadlem1  20593  lgsquadlem2  20594  dchrmusumlema  20642  rpvmasum2  20661  dchrisum0lema  20663  pntibndlem3  20741  pntlemi  20753  pntleml  20760  pnt3  20761  grpodiveq  20923  opidon  20989  issmgrp  21001  ismndo  21010  isrngo  21045  isdivrngo  21098  isvclem  21133  isnvlem  21166  isphg  21395  isph  21400  phoeqi  21436  ubthlem3  21451  minvecolem5  21460  minvecolem6  21461  minvecolem7  21462  hhph  21757  issh3  21799  nmopub  22488  nmfnleub  22505  adjeq  22515  adjvalval  22517  elunop2  22593  lnophm  22599  nmcexi  22606  cnlnadjlem5  22651  cnlnadjeui  22657  adjbd1o  22665  jpi  22850  mddmd2  22889  chrelati  22944  chrelat2i  22945  cvexchlem  22948  dmdbr5ati  23002  cdjreui  23012  cdj3i  23021  ballotlemfmpn  23053  eliccioo  23115  preqsnd  23194  abfmpunirn  23216  feqmptdf  23228  fmptcof2  23229  funcnvmptOLD  23234  funcnvmpt  23235  funcnv5mpt  23236  iocinioc2  23272  xrmulc1cn  23303  isrrvv  23646  eldmgm  23694  dmgmaddn0  23695  subfacp1lem3  23713  subfacp1lem6  23716  subfacp1  23717  txpcon  23763  sconpi1  23770  rescon  23777  cvmscbv  23789  cvmsval  23797  cvmlift2lem13  23846  cvmlift3lem2  23851  cvmlift3  23859  eupath2  23904  divelunit  24080  br8  24113  br6  24114  br4  24115  distel  24160  elpred  24177  poseq  24253  sltsolem1  24322  elfuns  24454  imageval  24469  dfrdg4  24488  altopthg  24501  altopthbg  24502  brbtwn  24527  brcgr  24528  brbtwn2  24533  colinearalg  24538  axeuclidlem  24590  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  brcolinear2  24681  lineext  24699  brsegle  24731  seglelin  24739  broutsideof2  24745  bpolyval  24784  onsuct0  24880  fnovpop  25038  twsymr  25078  prj1b  25079  prj3  25080  inttpemp  25139  repcpwti  25161  vecval1b  25451  svs2  25487  fgsb2  25555  islimrs3  25581  islimrs4  25582  bwt2  25592  supnuf  25629  supexr  25631  tcnvec  25690  ismgra  25710  isalg  25721  isded  25736  iscatOLD  25754  dualcat2  25784  issrc  25867  vtarsuelt  25895  sgplpte21a  26133  isibcg  26191  isfne4  26269  isfne2  26271  isfne3  26272  fneval  26287  topfneec  26291  neibastop2lem  26309  neibastop2  26310  neifg  26320  filnetlem4  26330  fdc  26455  heibor1  26534  rrncmslem  26556  rrnheibor  26561  isfldidl2  26694  isdmn3  26699  prtlem13  26736  prter3  26750  fnnfpeq0  26758  ralxpxfr2d  26760  ellz1  26846  lzunuz  26847  fz1eqin  26848  diophrex  26855  rexrabdioph  26875  rexfrabdioph  26876  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  fzneg  27069  expdioph  27116  wepwsolem  27138  fnwe2lem2  27148  islmodfg  27167  kercvrlsm  27181  dsmmelbas  27205  ellspd  27254  islindf  27282  islindf4  27308  f1omvdconj  27389  sdrgacs  27509  pm10.52  27560  iotasbc  27619  pm14.122a  27622  pm14.122b  27623  pm14.123a  27625  rusbcALT  27639  fvsb  27655  stoweidlem34  27783  2reu4a  27967  sbcfun  27985  funressnfv  27991  dfafn5a  28022  s2f1o  28091  nbcusgra  28159  uvtx01vtx  28164  cusgrauvtx  28168  frgra3vlem2  28179  gte-lte  28194  gt-lt  28195  bnj976  28809  bnj944  28970  bnj1173  29032  bnj1321  29057  bnj1373  29060  bnj1417  29071  lrelat  29204  islshpat  29207  lshpsmreu  29299  lkrpssN  29353  cmtvalN  29401  omllaw2N  29434  cvrval  29459  cvrval2  29464  cvlsupr3  29534  3dim0  29646  islln2  29700  islpln5  29724  islpln2  29725  islpln2ah  29738  islvol5  29768  islvol2  29769  4atlem11  29798  pmapglbx  29958  cdleme18d  30484  cdlemefrs29bpre0  30585  cdlemb3  30795  cdlemg33b  30896  dvhb1dimN  31175  dia11N  31238  cdlemm10N  31308  dib11N  31350  dib1dim  31355  dibglbN  31356  diblsmopel  31361  dihopelvalcpre  31438  dih11  31455  dihmeetlem4preN  31496  dihmeetlem13N  31509  lcfrvalsnN  31731  lcfrlem9  31740  lcf1o  31741  mapdval4N  31822  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  hdmap1fval  31987  hdmapfval  32020  hdmapglem7a  32120  hlhillcs  32151
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 177
  Copyright terms: Public domain W3C validator