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  1709  ax12olem6  1885  sbcom  2042  abbi  2406  necon3abid  2492  necon3bid  2494  necon1abid  2512  r19.21t  2641  ceqsralt  2824  ceqsrexv  2914  ceqsrex2v  2916  elab2g  2929  elrabf  2935  eueq2  2952  eqreu  2970  reu8  2974  ru  3003  sbcralt  3076  sbcabel  3081  csbnestgf  3142  disjpss  3518  ralprg  3695  rexprg  3696  difsn  3768  opthpr  3806  ralunsn  3831  dfiin2g  3952  iunxsng  3996  elpwuni  4005  disjxun  4037  pwnss  4192  opelopabt  4293  opelopabga  4294  brabga  4295  dfid3  4326  frirr  4386  wereu2  4406  ordtri4  4445  oneqmini  4459  elsucg  4475  elsuc2g  4476  dfwe2  4589  ssonprc  4599  ordpwsuc  4622  dfom2  4674  brab2a  4754  opeliunxp  4756  posn  4774  sosn  4775  frsn  4776  brab2ga  4779  opbrop  4783  elrnmpt1  4944  elrnmptg  4945  eliniseg2  5069  poleloe  5093  cnvpo  5229  dffun8  5297  fncnv  5330  fununi  5332  fnssresb  5372  fnimaeq0  5381  funcocnv2  5514  dffn5  5584  funimass4  5589  fnsnfv  5598  dmfco  5609  fndmdif  5645  fvimacnvi  5655  fvimacnvALT  5660  unpreima  5667  respreima  5670  fmptco  5707  fressnfv  5723  fnsuppres  5748  elunirnALT  5795  dff13  5799  fliftel  5824  isoini  5851  f1oiso  5864  f1oweALT  5867  eloprabga  5950  resoprab2  5957  ralrnmpt2  5974  ovid  5980  ov  5983  ovg  6002  ofrfval2  6112  fmpt2x  6206  ovmptss  6216  1stconst  6223  2ndconst  6224  brtpos2  6256  dfsmo2  6380  tfrlem1  6407  rdglim2  6461  seqomlem2  6479  omeu  6599  oeeui  6616  brdifun  6703  eqerlem  6708  brecop  6767  erovlem  6770  eceqoveq  6779  mapsn  6825  mptelixpg  6869  map1  6955  xpsnen  6962  xpdom2  6973  omxpenlem  6979  xpf1o  7039  mapunen  7046  onfin  7067  fimaxg  7120  fodomfib  7152  fofinf1o  7153  fipreima  7177  supub  7226  ordtypecbv  7248  ordtypelem3  7251  ordtypelem9  7257  hartogslem1  7273  wofib  7276  wemapso2lem  7281  wemapso2  7283  noinfep  7376  noinfepOLD  7377  cantnf  7411  rankbnd2  7557  domtri2  7638  infxpenc2  7665  fseqdom  7669  acni2  7689  dfac9  7778  cfeq0  7898  cfsuc  7899  cflim3  7904  cfslb  7908  cofsmo  7911  enfin2i  7963  isfin3ds  7971  isf33lem  8008  fin1a2lem5  8046  axdc2lem  8090  zorn2g  8146  fodomb  8167  brdom7disj  8172  brdom6disj  8173  iundom2g  8178  cfpwsdom  8222  elgch  8260  fpwwe2cbv  8268  fpwwecbv  8282  pwfseqlem3  8298  pwfseqlem4a  8299  pwfseqlem4  8300  ltpiord  8527  nlt1pi  8546  nqereu  8569  addclprlem1  8656  1idpr  8669  reclem3pr  8689  ltsosr  8732  map2psrpr  8748  supsrlem  8749  axrrecex  8801  xrlenlt  8906  addsubeq4  9082  renegcli  9124  lesub0  9306  wloglei  9321  conjmul  9493  rereccl  9494  infm3  9729  supmul1  9735  supmullem1  9736  supmullem2  9737  supmul  9738  creui  9757  nndiv  9802  elznn0  10054  prime  10108  eqreznegel  10319  zsupss  10323  rebtwnz  10331  ltxr  10473  elixx3g  10685  ixxun  10688  ioo0  10697  ico0  10718  ioc0  10719  icc0  10720  difreicc  10783  iccf1o  10794  elfz2  10805  fzn  10826  fznn  10868  fzshftral  10885  fzosplitsni  10937  om2uzisoi  11033  sq11i  11210  hashsdom  11379  wrdval  11432  cjreb  11624  rexfiuz  11847  cau3lem  11854  rlim2  11986  ello12  12006  ello1mpt  12011  elo12  12017  o1lo1  12027  lo1resb  12054  o1resb  12056  o1compt  12077  caucvgb  12168  mertens  12358  ruclem12  12535  divides  12549  odd2np1  12603  oddm1even  12604  sadadd2lem2  12657  gcdcllem2  12707  bezoutlem2  12734  bezoutlem3  12735  bezoutlem4  12736  isprm2  12782  isprm3  12783  prmreclem2  12980  prmreclem5  12983  prmreclem6  12984  4sqlem2  13012  4sqlem12  13019  vdwmc  13041  vdwpc  13043  vdwlem6  13049  vdwlem10  13053  vdwnn  13061  ramval  13071  0ram  13083  prdsleval  13392  pwsle  13407  imasleval  13459  xpsfrnel2  13483  xpsle  13499  isacs2  13571  mreacs  13576  acsfn  13577  iscatd2  13599  catpropd  13628  isssc  13713  evlfcl  14012  uncfcurf  14029  pltval  14110  lubid  14132  tosso  14158  oduleg  14252  oduclatb  14264  isipodrs  14280  odudlatb  14315  spwpr2  14353  spwex  14354  gsumvalx  14467  grplmulf1o  14558  grplactcnv  14580  elnmz  14672  eqgid  14685  isghm  14699  ghmeqker  14725  resscntz  14823  odmulgeq  14886  sylow3lem3  14956  sylow3lem6  14959  efgval2  15049  efgsdm  15055  efgrelexlema  15074  efgcpbllemb  15080  iscyggen2  15184  cyggenod  15187  eldprd  15255  dprdf11  15274  dprddisj2  15290  pgpfac1lem2  15326  pgpfac1  15331  drngid2  15544  issubrg  15561  islmod  15647  aspval2  16102  psrbag  16128  zndvds  16519  znleval  16524  iunocv  16597  pjfval2  16625  pjdm2  16627  istopg  16657  istpsOLD  16674  basgen2  16743  isclo  16840  mretopd  16845  isnei  16856  isperf3  16900  restdis  16925  restcls  16927  restlp  16929  restperf  16930  iscn  16981  iscnp  16983  lmbr2  17005  lmbrf  17006  ordtt1  17123  cmpsub  17143  hauscmplem  17149  cmpfi  17151  dfcon2  17161  1stcelcls  17203  1stccn  17205  nllyi  17217  subislly  17223  elkgen  17247  ptpjpre1  17282  ptuni2  17287  ptclsg  17325  ptcnplem  17331  txcn  17336  hausdiag  17355  txhaus  17357  txkgen  17362  xkoptsub  17364  cnmpt21  17381  elqtop  17404  tgqtop  17419  r0cld  17445  elfg  17582  fbasrn  17595  trfil2  17598  trfil3  17599  fin1aufil  17643  elfm2  17659  elfm3  17661  flimopn  17686  fbflim  17687  flfnei  17702  flftg  17707  cnpflf2  17711  txflf  17717  fclsbas  17732  alexsubALTlem4  17760  snclseqg  17814  tgphaus  17815  tsmsfbas  17826  tsmssubm  17841  prdsxmetlem  17948  imasdsf1olem  17953  xpsdsval  17961  blres  17993  isxms2  18010  metcnp  18103  txmetcnp  18109  txmetcn  18110  dscopn  18112  isngp4  18149  cnblcld  18300  metnrmlem1a  18378  icoopnst  18453  iocopnst  18454  elpi1  18559  lmmbr2  18701  cfil3i  18711  caucfil  18725  iscmet3  18735  lmclim  18744  metcld2  18748  bcthlem4  18765  minveclem3b  18808  minveclem6  18814  minveclem7  18815  ivthle  18832  ivthle2  18833  evthicc2  18836  ovolfioo  18843  ovolficc  18844  ovolgelb  18855  dyadmax  18969  subopnmbl  18975  ismbf3d  19025  mbfimaopnlem  19026  mbfimaopn2  19028  mbfaddlem  19031  mbfsup  19035  mbfinf  19036  i1f1lem  19060  i1fmulclem  19073  itg1climres  19085  mbfi1fseqlem4  19089  itg2monolem1  19121  itg2gt0  19131  isibl  19136  iblcnlem1  19158  ellimc2  19243  dvcnvrelem1  19380  itgsubst  19412  mdegleb  19466  fta1glem2  19568  quotval  19688  vieta1lem1  19706  vieta1lem2  19707  ulm2  19780  ulmcaulem  19787  ulmcau  19788  radcnvlt1  19810  sineq0  19905  cos11  19911  recosf1o  19913  efopn  20021  cxpeq  20113  mcubic  20159  birthdaylem3  20264  rlimcnp  20276  xrlimcnp  20279  wilth  20325  isppw  20368  isppw2  20369  mumullem2  20434  sqff1o  20436  dvdsmulf1o  20450  fsumvma  20468  fsumvma2  20469  vmasum  20471  chpchtsum  20474  lgsne0  20588  lgseisenlem2  20605  lgsquadlem1  20609  lgsquadlem2  20610  dchrmusumlema  20658  rpvmasum2  20677  dchrisum0lema  20679  pntibndlem3  20757  pntlemi  20769  pntleml  20776  pnt3  20777  grpodiveq  20939  opidon  21005  issmgrp  21017  ismndo  21026  isrngo  21061  isdivrngo  21114  isvclem  21149  isnvlem  21182  isphg  21411  isph  21416  phoeqi  21452  ubthlem3  21467  minvecolem5  21476  minvecolem6  21477  minvecolem7  21478  hhph  21773  issh3  21815  nmopub  22504  nmfnleub  22521  adjeq  22531  adjvalval  22533  elunop2  22609  lnophm  22615  nmcexi  22622  cnlnadjlem5  22667  cnlnadjeui  22673  adjbd1o  22681  jpi  22866  mddmd2  22905  chrelati  22960  chrelat2i  22961  cvexchlem  22964  dmdbr5ati  23018  cdjreui  23028  cdj3i  23037  ballotlemfmpn  23069  eliccioo  23131  preqsnd  23209  abfmpunirn  23231  feqmptdf  23243  fmptcof2  23244  funcnvmptOLD  23249  funcnvmpt  23250  funcnv5mpt  23251  iocinioc2  23287  xrmulc1cn  23318  isrrvv  23661  eldmgm  23709  dmgmaddn0  23710  subfacp1lem3  23728  subfacp1lem6  23731  subfacp1  23732  txpcon  23778  sconpi1  23785  rescon  23792  cvmscbv  23804  cvmsval  23812  cvmlift2lem13  23861  cvmlift3lem2  23866  cvmlift3  23874  eupath2  23919  divelunit  24095  br8  24184  br6  24185  br4  24186  distel  24231  elpred  24248  poseq  24324  sltsolem1  24393  elfuns  24525  imageval  24540  funpartfv  24555  dfrdg4  24560  altopthg  24573  altopthbg  24574  brbtwn  24599  brcgr  24600  brbtwn2  24605  colinearalg  24610  axeuclidlem  24662  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  brcolinear2  24753  lineext  24771  brsegle  24803  seglelin  24811  broutsideof2  24817  bpolyval  24856  onsuct0  24952  supaddc  24995  supadd  24996  itg2addnclem2  25004  fnovpop  25141  twsymr  25181  prj1b  25182  prj3  25183  inttpemp  25242  repcpwti  25264  vecval1b  25554  svs2  25590  fgsb2  25658  islimrs3  25684  islimrs4  25685  bwt2  25695  supnuf  25732  supexr  25734  tcnvec  25793  ismgra  25813  isalg  25824  isded  25839  iscatOLD  25857  dualcat2  25887  issrc  25970  vtarsuelt  25998  sgplpte21a  26236  isibcg  26294  isfne4  26372  isfne2  26374  isfne3  26375  fneval  26390  topfneec  26394  neibastop2lem  26412  neibastop2  26413  neifg  26423  filnetlem4  26433  fdc  26558  heibor1  26637  rrncmslem  26659  rrnheibor  26664  isfldidl2  26797  isdmn3  26802  prtlem13  26839  prter3  26853  fnnfpeq0  26861  ralxpxfr2d  26863  ellz1  26949  lzunuz  26950  fz1eqin  26951  diophrex  26958  rexrabdioph  26978  rexfrabdioph  26979  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  fzneg  27172  expdioph  27219  wepwsolem  27241  fnwe2lem2  27251  islmodfg  27270  kercvrlsm  27284  dsmmelbas  27308  ellspd  27357  islindf  27385  islindf4  27411  f1omvdconj  27492  sdrgacs  27612  pm10.52  27663  iotasbc  27722  pm14.122a  27725  pm14.122b  27726  pm14.123a  27728  rusbcALT  27742  fvsb  27758  stoweidlem34  27886  2reu4a  28070  sbcfun  28090  funressnfv  28096  dfafn5a  28128  isprmpt2  28208  s2f1o  28223  nbcusgra  28298  uvtx01vtx  28305  cusgrauvtx  28309  iswlk  28329  istrl  28336  ispth  28354  isspth  28355  wlkdvspthlem  28365  usgrcyclnl2  28387  frgra3vlem2  28425  gte-lte  28448  gt-lt  28449  bnj976  29125  bnj944  29286  bnj1173  29348  bnj1321  29373  bnj1373  29376  bnj1417  29387  ax12olem6NEW7  29436  sbcomwAUX7  29562  sbcomOLD7  29709  lrelat  29826  islshpat  29829  lshpsmreu  29921  lkrpssN  29975  cmtvalN  30023  omllaw2N  30056  cvrval  30081  cvrval2  30086  cvlsupr3  30156  3dim0  30268  islln2  30322  islpln5  30346  islpln2  30347  islpln2ah  30360  islvol5  30390  islvol2  30391  4atlem11  30420  pmapglbx  30580  cdleme18d  31106  cdlemefrs29bpre0  31207  cdlemb3  31417  cdlemg33b  31518  dvhb1dimN  31797  dia11N  31860  cdlemm10N  31930  dib11N  31972  dib1dim  31977  dibglbN  31978  diblsmopel  31983  dihopelvalcpre  32060  dih11  32077  dihmeetlem4preN  32118  dihmeetlem13N  32131  lcfrvalsnN  32353  lcfrlem9  32362  lcf1o  32363  mapdval4N  32444  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  hdmap1fval  32609  hdmapfval  32642  hdmapglem7a  32742  hlhillcs  32773
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