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  1698  ax12olem6  1875  sbcom  2028  abbi  2394  necon3abid  2480  necon3bid  2482  necon1abid  2500  r19.21t  2629  ceqsralt  2812  ceqsrexv  2902  ceqsrex2v  2904  elab2g  2917  elrabf  2923  eueq2  2940  eqreu  2958  reu8  2962  ru  2991  sbcralt  3064  sbcabel  3069  csbnestgf  3130  disjpss  3506  ralprg  3683  rexprg  3684  difsn  3756  opthpr  3791  ralunsn  3816  dfiin2g  3937  iunxsng  3981  elpwuni  3990  disjxun  4022  opelopabt  4276  opelopabga  4277  brabga  4278  dfid3  4309  frirr  4369  wereu2  4389  ordtri4  4428  oneqmini  4442  elsucg  4458  elsuc2g  4459  dfwe2  4572  ssonprc  4582  ordpwsuc  4605  dfom2  4657  brab2a  4737  opeliunxp  4739  posn  4757  sosn  4758  frsn  4759  brab2ga  4762  opbrop  4766  elrnmpt1  4927  elrnmptg  4928  eliniseg2  5052  poleloe  5076  cnvpo  5211  dffun8  5247  fncnv  5280  fununi  5282  fnssresb  5322  fnimaeq0  5331  funcocnv2  5464  dffn5  5530  funimass4  5535  fnsnfv  5544  dmfco  5555  fndmdif  5591  fvimacnvi  5601  fvimacnvALT  5606  unpreima  5613  respreima  5616  fmptco  5653  fressnfv  5669  fnsuppres  5694  elunirnALT  5741  dff13  5745  fliftel  5770  isoini  5797  f1oiso  5810  f1oweALT  5813  eloprabga  5896  resoprab2  5903  ralrnmpt2  5920  ovid  5926  ov  5929  ovg  5948  ofrfval2  6058  fmpt2x  6152  ovmptss  6162  1stconst  6169  2ndconst  6170  brtpos2  6202  pwnss  6293  dfsmo2  6360  tfrlem1  6387  rdglim2  6441  seqomlem2  6459  omeu  6579  oeeui  6596  brdifun  6683  eqerlem  6688  brecop  6747  erovlem  6750  eceqoveq  6759  mapsn  6805  mptelixpg  6849  map1  6935  xpsnen  6942  xpdom2  6953  omxpenlem  6959  xpf1o  7019  mapunen  7026  onfin  7047  fimaxg  7100  fodomfib  7132  fofinf1o  7133  fipreima  7157  supub  7206  ordtypecbv  7228  ordtypelem3  7231  ordtypelem9  7237  hartogslem1  7253  wofib  7256  wemapso2lem  7261  wemapso2  7263  noinfep  7356  noinfepOLD  7357  cantnf  7391  rankbnd2  7537  domtri2  7618  infxpenc2  7645  fseqdom  7649  acni2  7669  dfac9  7758  cfeq0  7878  cfsuc  7879  cflim3  7884  cfslb  7888  cofsmo  7891  enfin2i  7943  isfin3ds  7951  isf33lem  7988  fin1a2lem5  8026  axdc2lem  8070  zorn2g  8126  fodomb  8147  brdom7disj  8152  brdom6disj  8153  iundom2g  8158  cfpwsdom  8202  elgch  8240  fpwwe2cbv  8248  fpwwecbv  8262  pwfseqlem3  8278  pwfseqlem4a  8279  pwfseqlem4  8280  ltpiord  8507  nlt1pi  8526  nqereu  8549  addclprlem1  8636  1idpr  8649  reclem3pr  8669  ltsosr  8712  map2psrpr  8728  supsrlem  8729  axrrecex  8781  xrlenlt  8886  addsubeq4  9062  renegcli  9104  lesub0  9286  wloglei  9301  conjmul  9473  rereccl  9474  infm3  9709  supmul1  9715  supmullem1  9716  supmullem2  9717  supmul  9718  creui  9737  nndiv  9782  elznn0  10034  prime  10088  eqreznegel  10299  zsupss  10303  rebtwnz  10311  ltxr  10453  elixx3g  10665  ixxun  10668  ioo0  10677  ico0  10698  ioc0  10699  icc0  10700  difreicc  10763  iccf1o  10774  elfz2  10785  fzn  10806  fznn  10848  fzshftral  10865  fzosplitsni  10917  om2uzisoi  11013  sq11i  11190  hashsdom  11359  wrdval  11412  cjreb  11604  rexfiuz  11827  cau3lem  11834  rlim2  11966  ello12  11986  ello1mpt  11991  elo12  11997  o1lo1  12007  lo1resb  12034  o1resb  12036  o1compt  12057  caucvgb  12148  mertens  12338  ruclem12  12515  divides  12529  odd2np1  12583  oddm1even  12584  sadadd2lem2  12637  gcdcllem2  12687  bezoutlem2  12714  bezoutlem3  12715  bezoutlem4  12716  isprm2  12762  isprm3  12763  prmreclem2  12960  prmreclem5  12963  prmreclem6  12964  4sqlem2  12992  4sqlem12  12999  vdwmc  13021  vdwpc  13023  vdwlem6  13029  vdwlem10  13033  vdwnn  13041  ramval  13051  0ram  13063  prdsleval  13372  pwsle  13387  imasleval  13439  xpsfrnel2  13463  xpsle  13479  isacs2  13551  mreacs  13556  acsfn  13557  iscatd2  13579  catpropd  13608  isssc  13693  evlfcl  13992  uncfcurf  14009  pltval  14090  lubid  14112  tosso  14138  oduleg  14232  oduclatb  14244  isipodrs  14260  odudlatb  14295  spwpr2  14333  spwex  14334  gsumvalx  14447  grplmulf1o  14538  grplactcnv  14560  elnmz  14652  eqgid  14665  isghm  14679  ghmeqker  14705  resscntz  14803  odmulgeq  14866  sylow3lem3  14936  sylow3lem6  14939  efgval2  15029  efgsdm  15035  efgrelexlema  15054  efgcpbllemb  15060  iscyggen2  15164  cyggenod  15167  eldprd  15235  dprdf11  15254  dprddisj2  15270  pgpfac1lem2  15306  pgpfac1  15311  drngid2  15524  issubrg  15541  islmod  15627  aspval2  16082  psrbag  16108  zndvds  16499  znleval  16504  iunocv  16577  pjfval2  16605  pjdm2  16607  istopg  16637  istpsOLD  16654  basgen2  16723  isclo  16820  mretopd  16825  isnei  16836  isperf3  16880  restdis  16905  restcls  16907  restlp  16909  restperf  16910  iscn  16961  iscnp  16963  lmbr2  16985  lmbrf  16986  ordtt1  17103  cmpsub  17123  hauscmplem  17129  cmpfi  17131  dfcon2  17141  1stcelcls  17183  1stccn  17185  nllyi  17197  subislly  17203  elkgen  17227  ptpjpre1  17262  ptuni2  17267  ptclsg  17305  ptcnplem  17311  txcn  17316  hausdiag  17335  txhaus  17337  txkgen  17342  xkoptsub  17344  cnmpt21  17361  elqtop  17384  tgqtop  17399  r0cld  17425  elfg  17562  fbasrn  17575  trfil2  17578  trfil3  17579  fin1aufil  17623  elfm2  17639  elfm3  17641  flimopn  17666  fbflim  17667  flfnei  17682  flftg  17687  cnpflf2  17691  txflf  17697  fclsbas  17712  alexsubALTlem4  17740  snclseqg  17794  tgphaus  17795  tsmsfbas  17806  tsmssubm  17821  prdsxmetlem  17928  imasdsf1olem  17933  xpsdsval  17941  blres  17973  isxms2  17990  metcnp  18083  txmetcnp  18089  txmetcn  18090  dscopn  18092  isngp4  18129  cnblcld  18280  metnrmlem1a  18358  icoopnst  18433  iocopnst  18434  elpi1  18539  lmmbr2  18681  cfil3i  18691  caucfil  18705  iscmet3  18715  lmclim  18724  metcld2  18728  bcthlem4  18745  minveclem3b  18788  minveclem6  18794  minveclem7  18795  ivthle  18812  ivthle2  18813  evthicc2  18816  ovolfioo  18823  ovolficc  18824  ovolgelb  18835  dyadmax  18949  subopnmbl  18955  ismbf3d  19005  mbfimaopnlem  19006  mbfimaopn2  19008  mbfaddlem  19011  mbfsup  19015  mbfinf  19016  i1f1lem  19040  i1fmulclem  19053  itg1climres  19065  mbfi1fseqlem4  19069  itg2monolem1  19101  itg2gt0  19111  isibl  19116  iblcnlem1  19138  ellimc2  19223  dvcnvrelem1  19360  itgsubst  19392  mdegleb  19446  fta1glem2  19548  quotval  19668  vieta1lem1  19686  vieta1lem2  19687  ulm2  19760  ulmcaulem  19767  ulmcau  19768  radcnvlt1  19790  sineq0  19885  cos11  19891  recosf1o  19893  efopn  20001  cxpeq  20093  mcubic  20139  birthdaylem3  20244  rlimcnp  20256  xrlimcnp  20259  wilth  20305  isppw  20348  isppw2  20349  mumullem2  20414  sqff1o  20416  dvdsmulf1o  20430  fsumvma  20448  fsumvma2  20449  vmasum  20451  chpchtsum  20454  lgsne0  20568  lgseisenlem2  20585  lgsquadlem1  20589  lgsquadlem2  20590  dchrmusumlema  20638  rpvmasum2  20657  dchrisum0lema  20659  pntibndlem3  20737  pntlemi  20749  pntleml  20756  pnt3  20757  grpodiveq  20917  opidon  20983  issmgrp  20995  ismndo  21004  isrngo  21039  isdivrngo  21092  isvclem  21127  isnvlem  21160  isphg  21389  isph  21394  phoeqi  21430  ubthlem3  21445  minvecolem5  21454  minvecolem6  21455  minvecolem7  21456  hhph  21753  issh3  21795  nmopub  22484  nmfnleub  22501  adjeq  22511  adjvalval  22513  elunop2  22589  lnophm  22595  nmcexi  22602  cnlnadjlem5  22647  cnlnadjeui  22653  adjbd1o  22661  jpi  22846  mddmd2  22885  chrelati  22940  chrelat2i  22941  cvexchlem  22944  dmdbr5ati  22998  cdjreui  23008  cdj3i  23017  ballotlemfmpn  23049  eldmgm  23101  dmgmaddn0  23102  subfacp1lem3  23120  subfacp1lem6  23123  subfacp1  23124  txpcon  23170  sconpi1  23177  rescon  23184  cvmscbv  23196  cvmsval  23204  cvmlift2lem13  23253  cvmlift3lem2  23258  cvmlift3  23266  eupath2  23311  divelunit  23486  br8  23519  br6  23520  br4  23521  distel  23564  elpred  23581  poseq  23657  axsltsolem1  23725  axfelem20  23769  imageval  23879  dfrdg4  23898  altopthg  23911  altopthbg  23912  brbtwn  23937  brcgr  23938  brbtwn2  23943  colinearalg  23948  axeuclidlem  24000  axcontlem2  24003  axcontlem4  24005  axcontlem7  24008  brcolinear2  24091  lineext  24109  brsegle  24141  seglelin  24149  broutsideof2  24155  bpolyval  24194  onsuct0  24290  fnovpop  24448  twsymr  24488  prj1b  24489  prj3  24490  inttpemp  24550  repcpwti  24572  vecval1b  24862  svs2  24898  fgsb2  24966  islimrs3  24992  islimrs4  24993  bwt2  25003  supnuf  25040  supexr  25042  tcnvec  25101  ismgra  25121  isalg  25132  isded  25147  iscatOLD  25165  dualcat2  25195  issrc  25278  vtarsuelt  25306  sgplpte21a  25544  isibcg  25602  isfne4  25680  isfne2  25682  isfne3  25683  fneval  25698  topfneec  25702  neibastop2lem  25720  neibastop2  25721  neifg  25731  filnetlem4  25741  fdc  25866  heibor1  25945  rrncmslem  25967  rrnheibor  25972  isfldidl2  26105  isdmn3  26110  prtlem13  26147  prter3  26161  fnnfpeq0  26169  ralxpxfr2d  26171  ellz1  26257  lzunuz  26258  fz1eqin  26259  diophrex  26266  rexrabdioph  26286  rexfrabdioph  26287  2rexfrabdioph  26288  3rexfrabdioph  26289  4rexfrabdioph  26290  6rexfrabdioph  26291  7rexfrabdioph  26292  fzneg  26480  expdioph  26527  wepwsolem  26549  fnwe2lem2  26559  islmodfg  26578  kercvrlsm  26592  dsmmelbas  26616  ellspd  26665  islindf  26693  islindf4  26719  f1omvdconj  26800  sdrgacs  26920  pm10.52  26971  iotasbc  27030  pm14.122a  27033  pm14.122b  27034  pm14.123a  27036  rusbcALT  27050  fvsb  27066  stoweidlem34  27194  2reu4a  27358  sbcfun  27376  funressnfv  27382  dfafn5a  27413  gte-lte  27466  gt-lt  27467  bnj976  28088  bnj944  28249  bnj1173  28311  bnj1321  28336  bnj1373  28339  bnj1417  28350  lrelat  28483  islshpat  28486  lshpsmreu  28578  lkrpssN  28632  cmtvalN  28680  omllaw2N  28713  cvrval  28738  cvrval2  28743  cvlsupr3  28813  3dim0  28925  islln2  28979  islpln5  29003  islpln2  29004  islpln2ah  29017  islvol5  29047  islvol2  29048  4atlem11  29077  pmapglbx  29237  cdleme18d  29763  cdlemefrs29bpre0  29864  cdlemb3  30074  cdlemg33b  30175  dvhb1dimN  30454  dia11N  30517  cdlemm10N  30587  dib11N  30629  dib1dim  30634  dibglbN  30635  diblsmopel  30640  dihopelvalcpre  30717  dih11  30734  dihmeetlem4preN  30775  dihmeetlem13N  30788  lcfrvalsnN  31010  lcfrlem9  31019  lcf1o  31020  mapdval4N  31101  baerlem3lem2  31179  baerlem5alem2  31180  baerlem5blem2  31181  hdmap1fval  31266  hdmapfval  31299  hdmapglem7a  31399  hlhillcs  31430
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