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  1699  ax12olem6  1875  sbcom  2031  abbi  2395  necon3abid  2481  necon3bid  2483  necon1abid  2501  r19.21t  2630  ceqsralt  2813  ceqsrexv  2903  ceqsrex2v  2905  elab2g  2918  elrabf  2924  eueq2  2941  eqreu  2959  reu8  2963  ru  2992  sbcralt  3065  sbcabel  3070  csbnestgf  3131  disjpss  3507  ralprg  3684  rexprg  3685  difsn  3757  opthpr  3792  ralunsn  3817  dfiin2g  3938  iunxsng  3982  elpwuni  3991  disjxun  4023  pwnss  4178  opelopabt  4279  opelopabga  4280  brabga  4281  dfid3  4312  frirr  4372  wereu2  4392  ordtri4  4431  oneqmini  4445  elsucg  4461  elsuc2g  4462  dfwe2  4575  ssonprc  4585  ordpwsuc  4608  dfom2  4660  brab2a  4740  opeliunxp  4742  posn  4760  sosn  4761  frsn  4762  brab2ga  4765  opbrop  4769  elrnmpt1  4930  elrnmptg  4931  eliniseg2  5055  poleloe  5079  cnvpo  5215  dffun8  5283  fncnv  5316  fununi  5318  fnssresb  5358  fnimaeq0  5367  funcocnv2  5500  dffn5  5570  funimass4  5575  fnsnfv  5584  dmfco  5595  fndmdif  5631  fvimacnvi  5641  fvimacnvALT  5646  unpreima  5653  respreima  5656  fmptco  5693  fressnfv  5709  fnsuppres  5734  elunirnALT  5781  dff13  5785  fliftel  5810  isoini  5837  f1oiso  5850  f1oweALT  5853  eloprabga  5936  resoprab2  5943  ralrnmpt2  5960  ovid  5966  ov  5969  ovg  5988  ofrfval2  6098  fmpt2x  6192  ovmptss  6202  1stconst  6209  2ndconst  6210  brtpos2  6242  dfsmo2  6366  tfrlem1  6393  rdglim2  6447  seqomlem2  6465  omeu  6585  oeeui  6602  brdifun  6689  eqerlem  6694  brecop  6753  erovlem  6756  eceqoveq  6765  mapsn  6811  mptelixpg  6855  map1  6941  xpsnen  6948  xpdom2  6959  omxpenlem  6965  xpf1o  7025  mapunen  7032  onfin  7053  fimaxg  7106  fodomfib  7138  fofinf1o  7139  fipreima  7163  supub  7212  ordtypecbv  7234  ordtypelem3  7237  ordtypelem9  7243  hartogslem1  7259  wofib  7262  wemapso2lem  7267  wemapso2  7269  noinfep  7362  noinfepOLD  7363  cantnf  7397  rankbnd2  7543  domtri2  7624  infxpenc2  7651  fseqdom  7655  acni2  7675  dfac9  7764  cfeq0  7884  cfsuc  7885  cflim3  7890  cfslb  7894  cofsmo  7897  enfin2i  7949  isfin3ds  7957  isf33lem  7994  fin1a2lem5  8032  axdc2lem  8076  zorn2g  8132  fodomb  8153  brdom7disj  8158  brdom6disj  8159  iundom2g  8164  cfpwsdom  8208  elgch  8246  fpwwe2cbv  8254  fpwwecbv  8268  pwfseqlem3  8284  pwfseqlem4a  8285  pwfseqlem4  8286  ltpiord  8513  nlt1pi  8532  nqereu  8555  addclprlem1  8642  1idpr  8655  reclem3pr  8675  ltsosr  8718  map2psrpr  8734  supsrlem  8735  axrrecex  8787  xrlenlt  8892  addsubeq4  9068  renegcli  9110  lesub0  9292  wloglei  9307  conjmul  9479  rereccl  9480  infm3  9715  supmul1  9721  supmullem1  9722  supmullem2  9723  supmul  9724  creui  9743  nndiv  9788  elznn0  10040  prime  10094  eqreznegel  10305  zsupss  10309  rebtwnz  10317  ltxr  10459  elixx3g  10671  ixxun  10674  ioo0  10683  ico0  10704  ioc0  10705  icc0  10706  difreicc  10769  iccf1o  10780  elfz2  10791  fzn  10812  fznn  10854  fzshftral  10871  fzosplitsni  10923  om2uzisoi  11019  sq11i  11196  hashsdom  11365  wrdval  11418  cjreb  11610  rexfiuz  11833  cau3lem  11840  rlim2  11972  ello12  11992  ello1mpt  11997  elo12  12003  o1lo1  12013  lo1resb  12040  o1resb  12042  o1compt  12063  caucvgb  12154  mertens  12344  ruclem12  12521  divides  12535  odd2np1  12589  oddm1even  12590  sadadd2lem2  12643  gcdcllem2  12693  bezoutlem2  12720  bezoutlem3  12721  bezoutlem4  12722  isprm2  12768  isprm3  12769  prmreclem2  12966  prmreclem5  12969  prmreclem6  12970  4sqlem2  12998  4sqlem12  13005  vdwmc  13027  vdwpc  13029  vdwlem6  13035  vdwlem10  13039  vdwnn  13047  ramval  13057  0ram  13069  prdsleval  13378  pwsle  13393  imasleval  13445  xpsfrnel2  13469  xpsle  13485  isacs2  13557  mreacs  13562  acsfn  13563  iscatd2  13585  catpropd  13614  isssc  13699  evlfcl  13998  uncfcurf  14015  pltval  14096  lubid  14118  tosso  14144  oduleg  14238  oduclatb  14250  isipodrs  14266  odudlatb  14301  spwpr2  14339  spwex  14340  gsumvalx  14453  grplmulf1o  14544  grplactcnv  14566  elnmz  14658  eqgid  14671  isghm  14685  ghmeqker  14711  resscntz  14809  odmulgeq  14872  sylow3lem3  14942  sylow3lem6  14945  efgval2  15035  efgsdm  15041  efgrelexlema  15060  efgcpbllemb  15066  iscyggen2  15170  cyggenod  15173  eldprd  15241  dprdf11  15260  dprddisj2  15276  pgpfac1lem2  15312  pgpfac1  15317  drngid2  15530  issubrg  15547  islmod  15633  aspval2  16088  psrbag  16114  zndvds  16505  znleval  16510  iunocv  16583  pjfval2  16611  pjdm2  16613  istopg  16643  istpsOLD  16660  basgen2  16729  isclo  16826  mretopd  16831  isnei  16842  isperf3  16886  restdis  16911  restcls  16913  restlp  16915  restperf  16916  iscn  16967  iscnp  16969  lmbr2  16991  lmbrf  16992  ordtt1  17109  cmpsub  17129  hauscmplem  17135  cmpfi  17137  dfcon2  17147  1stcelcls  17189  1stccn  17191  nllyi  17203  subislly  17209  elkgen  17233  ptpjpre1  17268  ptuni2  17273  ptclsg  17311  ptcnplem  17317  txcn  17322  hausdiag  17341  txhaus  17343  txkgen  17348  xkoptsub  17350  cnmpt21  17367  elqtop  17390  tgqtop  17405  r0cld  17431  elfg  17568  fbasrn  17581  trfil2  17584  trfil3  17585  fin1aufil  17629  elfm2  17645  elfm3  17647  flimopn  17672  fbflim  17673  flfnei  17688  flftg  17693  cnpflf2  17697  txflf  17703  fclsbas  17718  alexsubALTlem4  17746  snclseqg  17800  tgphaus  17801  tsmsfbas  17812  tsmssubm  17827  prdsxmetlem  17934  imasdsf1olem  17939  xpsdsval  17947  blres  17979  isxms2  17996  metcnp  18089  txmetcnp  18095  txmetcn  18096  dscopn  18098  isngp4  18135  cnblcld  18286  metnrmlem1a  18364  icoopnst  18439  iocopnst  18440  elpi1  18545  lmmbr2  18687  cfil3i  18697  caucfil  18711  iscmet3  18721  lmclim  18730  metcld2  18734  bcthlem4  18751  minveclem3b  18794  minveclem6  18800  minveclem7  18801  ivthle  18818  ivthle2  18819  evthicc2  18822  ovolfioo  18829  ovolficc  18830  ovolgelb  18841  dyadmax  18955  subopnmbl  18961  ismbf3d  19011  mbfimaopnlem  19012  mbfimaopn2  19014  mbfaddlem  19017  mbfsup  19021  mbfinf  19022  i1f1lem  19046  i1fmulclem  19059  itg1climres  19071  mbfi1fseqlem4  19075  itg2monolem1  19107  itg2gt0  19117  isibl  19122  iblcnlem1  19144  ellimc2  19229  dvcnvrelem1  19366  itgsubst  19398  mdegleb  19452  fta1glem2  19554  quotval  19674  vieta1lem1  19692  vieta1lem2  19693  ulm2  19766  ulmcaulem  19773  ulmcau  19774  radcnvlt1  19796  sineq0  19891  cos11  19897  recosf1o  19899  efopn  20007  cxpeq  20099  mcubic  20145  birthdaylem3  20250  rlimcnp  20262  xrlimcnp  20265  wilth  20311  isppw  20354  isppw2  20355  mumullem2  20420  sqff1o  20422  dvdsmulf1o  20436  fsumvma  20454  fsumvma2  20455  vmasum  20457  chpchtsum  20460  lgsne0  20574  lgseisenlem2  20591  lgsquadlem1  20595  lgsquadlem2  20596  dchrmusumlema  20644  rpvmasum2  20663  dchrisum0lema  20665  pntibndlem3  20743  pntlemi  20755  pntleml  20762  pnt3  20763  grpodiveq  20925  opidon  20991  issmgrp  21003  ismndo  21012  isrngo  21047  isdivrngo  21100  isvclem  21135  isnvlem  21168  isphg  21397  isph  21402  phoeqi  21438  ubthlem3  21453  minvecolem5  21462  minvecolem6  21463  minvecolem7  21464  hhph  21759  issh3  21801  nmopub  22490  nmfnleub  22507  adjeq  22517  adjvalval  22519  elunop2  22595  lnophm  22601  nmcexi  22608  cnlnadjlem5  22653  cnlnadjeui  22659  adjbd1o  22667  jpi  22852  mddmd2  22891  chrelati  22946  chrelat2i  22947  cvexchlem  22950  dmdbr5ati  23004  cdjreui  23014  cdj3i  23023  ballotlemfmpn  23055  eliccioo  23117  preqsnd  23196  abfmpunirn  23218  feqmptdf  23230  fmptcof2  23231  funcnvmptOLD  23236  funcnvmpt  23237  funcnv5mpt  23238  iocinioc2  23274  xrmulc1cn  23305  isrrvv  23648  eldmgm  23696  dmgmaddn0  23697  subfacp1lem3  23715  subfacp1lem6  23718  subfacp1  23719  txpcon  23765  sconpi1  23772  rescon  23779  cvmscbv  23791  cvmsval  23799  cvmlift2lem13  23848  cvmlift3lem2  23853  cvmlift3  23861  eupath2  23906  divelunit  24082  br8  24115  br6  24116  br4  24117  distel  24162  elpred  24179  poseq  24255  sltsolem1  24324  elfuns  24456  imageval  24471  dfrdg4  24490  altopthg  24503  altopthbg  24504  brbtwn  24529  brcgr  24530  brbtwn2  24535  colinearalg  24540  axeuclidlem  24592  axcontlem2  24595  axcontlem4  24597  axcontlem7  24600  brcolinear2  24683  lineext  24701  brsegle  24733  seglelin  24741  broutsideof2  24747  bpolyval  24786  onsuct0  24882  supaddc  24927  supadd  24928  itg2addnclem2  24934  fnovpop  25049  twsymr  25089  prj1b  25090  prj3  25091  inttpemp  25150  repcpwti  25172  vecval1b  25462  svs2  25498  fgsb2  25566  islimrs3  25592  islimrs4  25593  bwt2  25603  supnuf  25640  supexr  25642  tcnvec  25701  ismgra  25721  isalg  25732  isded  25747  iscatOLD  25765  dualcat2  25795  issrc  25878  vtarsuelt  25906  sgplpte21a  26144  isibcg  26202  isfne4  26280  isfne2  26282  isfne3  26283  fneval  26298  topfneec  26302  neibastop2lem  26320  neibastop2  26321  neifg  26331  filnetlem4  26341  fdc  26466  heibor1  26545  rrncmslem  26567  rrnheibor  26572  isfldidl2  26705  isdmn3  26710  prtlem13  26747  prter3  26761  fnnfpeq0  26769  ralxpxfr2d  26771  ellz1  26857  lzunuz  26858  fz1eqin  26859  diophrex  26866  rexrabdioph  26886  rexfrabdioph  26887  2rexfrabdioph  26888  3rexfrabdioph  26889  4rexfrabdioph  26890  6rexfrabdioph  26891  7rexfrabdioph  26892  fzneg  27080  expdioph  27127  wepwsolem  27149  fnwe2lem2  27159  islmodfg  27178  kercvrlsm  27192  dsmmelbas  27216  ellspd  27265  islindf  27293  islindf4  27319  f1omvdconj  27400  sdrgacs  27520  pm10.52  27571  iotasbc  27630  pm14.122a  27633  pm14.122b  27634  pm14.123a  27636  rusbcALT  27650  fvsb  27666  stoweidlem34  27794  2reu4a  27978  sbcfun  27996  funressnfv  28002  dfafn5a  28033  s2f1o  28102  nbcusgra  28170  uvtx01vtx  28175  cusgrauvtx  28179  frgra3vlem2  28190  gte-lte  28205  gt-lt  28206  bnj976  28882  bnj944  29043  bnj1173  29105  bnj1321  29130  bnj1373  29133  bnj1417  29144  lrelat  29277  islshpat  29280  lshpsmreu  29372  lkrpssN  29426  cmtvalN  29474  omllaw2N  29507  cvrval  29532  cvrval2  29537  cvlsupr3  29607  3dim0  29719  islln2  29773  islpln5  29797  islpln2  29798  islpln2ah  29811  islvol5  29841  islvol2  29842  4atlem11  29871  pmapglbx  30031  cdleme18d  30557  cdlemefrs29bpre0  30658  cdlemb3  30868  cdlemg33b  30969  dvhb1dimN  31248  dia11N  31311  cdlemm10N  31381  dib11N  31423  dib1dim  31428  dibglbN  31429  diblsmopel  31434  dihopelvalcpre  31511  dih11  31528  dihmeetlem4preN  31569  dihmeetlem13N  31582  lcfrvalsnN  31804  lcfrlem9  31813  lcf1o  31814  mapdval4N  31895  baerlem3lem2  31973  baerlem5alem2  31974  baerlem5blem2  31975  hdmap1fval  32060  hdmapfval  32093  hdmapglem7a  32193  hlhillcs  32224
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