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

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
StepHypRef Expression
1 syl5bb.1 . . 3  |-  ( ph  <->  ps )
21a1i 11 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
3 syl5bb.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3bitrd 245 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  syl5rbb  250  syl5bbr  251  3bitr4g  280  imim21b  357  cad0  1406  had1  1408  ax11wdemo  1730  ax12olem6OLD  1962  sbcom  2115  abbi  2490  necon3abid  2576  necon3bid  2578  necon1abid  2596  r19.21t  2727  ceqsralt  2915  ceqsrexv  3005  ceqsrex2v  3007  elab2g  3020  elrabf  3027  eueq2  3044  eqreu  3062  reu8  3066  ru  3096  sbcralt  3169  csbnestgf  3235  disjpss  3614  ralprg  3793  rexprg  3794  difsn  3869  opthpr  3911  ralunsn  3938  dfiin2g  4059  iunxsng  4103  elpwuni  4112  disjxun  4144  pwnss  4299  opelopabt  4401  opelopabga  4402  brabga  4403  dfid3  4433  frirr  4493  wereu2  4513  ordtri4  4552  oneqmini  4566  elsucg  4582  elsuc2g  4583  dfwe2  4695  ssonprc  4705  ordpwsuc  4728  dfom2  4780  brab2a  4860  opeliunxp  4862  posn  4879  sosn  4880  frsn  4881  brab2ga  4884  opbrop  4888  elrnmpt1  5052  elrnmptg  5053  eliniseg2  5177  poleloe  5201  cnvpo  5343  dffun8  5413  fncnv  5448  fununi  5450  fnssresb  5490  fnimaeq0  5499  funcocnv2  5633  dffn5  5704  funimass4  5709  fnsnfv  5718  dmfco  5729  fndmdif  5766  fvimacnvi  5776  fvimacnvALT  5781  unpreima  5788  respreima  5791  fmptco  5833  fressnfv  5852  fnsuppres  5884  elunirnALT  5932  dff13  5936  fliftel  5963  isoini  5990  f1oiso  6003  f1oweALT  6006  eloprabga  6092  resoprab2  6099  ralrnmpt2  6116  ovid  6122  ov  6125  ovg  6144  ofrfval2  6255  fmpt2x  6349  ovmptss  6360  1stconst  6367  2ndconst  6368  isprmpt2  6406  brtpos2  6414  dfsmo2  6538  tfrlem1  6565  rdglim2  6619  seqomlem2  6637  omeu  6757  oeeui  6774  brdifun  6861  eqerlem  6866  brecop  6926  erovlem  6929  eceqoveq  6938  mapsn  6984  mptelixpg  7028  map1  7114  xpsnen  7121  xpdom2  7132  omxpenlem  7138  xpf1o  7198  mapunen  7205  onfin  7226  fimaxg  7283  fodomfib  7315  fofinf1o  7316  fipreima  7340  supub  7390  ordtypecbv  7412  ordtypelem3  7415  ordtypelem9  7421  hartogslem1  7437  wofib  7440  wemapso2lem  7445  wemapso2  7447  noinfep  7540  noinfepOLD  7541  cantnf  7575  rankbnd2  7721  domtri2  7802  infxpenc2  7829  fseqdom  7833  acni2  7853  dfac9  7942  cfeq0  8062  cfsuc  8063  cflim3  8068  cfslb  8072  cofsmo  8075  enfin2i  8127  isfin3ds  8135  isf33lem  8172  fin1a2lem5  8210  axdc2lem  8254  zorn2g  8309  fodomb  8330  brdom7disj  8335  brdom6disj  8336  iundom2g  8341  cfpwsdom  8385  elgch  8423  fpwwe2cbv  8431  fpwwecbv  8445  pwfseqlem3  8461  pwfseqlem4a  8462  pwfseqlem4  8463  ltpiord  8690  nlt1pi  8709  nqereu  8732  addclprlem1  8819  1idpr  8832  reclem3pr  8852  ltsosr  8895  map2psrpr  8911  supsrlem  8912  axrrecex  8964  xrlenlt  9069  addsubeq4  9245  renegcli  9287  lesub0  9469  wloglei  9484  conjmul  9656  rereccl  9657  infm3  9892  supmul1  9898  supmullem1  9899  supmullem2  9900  supmul  9901  creui  9920  nndiv  9965  elznn0  10221  prime  10275  eqreznegel  10486  zsupss  10490  rebtwnz  10498  ltxr  10640  elixx3g  10854  ixxun  10857  ioo0  10866  ico0  10887  ioc0  10888  icc0  10889  difreicc  10953  iccf1o  10964  elfz2  10975  fzn  10996  fznn  11038  fzshftral  11057  fzosplitsni  11116  om2uzisoi  11214  sq11i  11392  hashsdom  11575  brfi1uzind  11635  wrdval  11650  s2f1o  11783  cjreb  11848  rexfiuz  12071  cau3lem  12078  rlim2  12210  ello12  12230  ello1mpt  12235  elo12  12241  o1lo1  12251  lo1resb  12278  o1resb  12280  o1compt  12301  caucvgb  12393  mertens  12583  ruclem12  12760  divides  12774  odd2np1  12828  oddm1even  12829  sadadd2lem2  12882  gcdcllem2  12932  bezoutlem2  12959  bezoutlem3  12960  bezoutlem4  12961  isprm2  13007  isprm3  13008  prmreclem2  13205  prmreclem5  13208  prmreclem6  13209  4sqlem2  13237  4sqlem12  13244  vdwmc  13266  vdwpc  13268  vdwlem6  13274  vdwlem10  13278  vdwnn  13286  ramval  13296  0ram  13308  prdsleval  13619  pwsle  13634  imasleval  13686  xpsfrnel2  13710  xpsle  13726  isacs2  13798  mreacs  13803  acsfn  13804  iscatd2  13826  catpropd  13855  isssc  13940  evlfcl  14239  uncfcurf  14256  pltval  14337  lubid  14359  tosso  14385  oduleg  14479  oduclatb  14491  isipodrs  14507  odudlatb  14542  spwpr2  14580  spwex  14581  gsumvalx  14694  grplmulf1o  14785  grplactcnv  14807  elnmz  14899  eqgid  14912  isghm  14926  ghmeqker  14952  resscntz  15050  odmulgeq  15113  sylow3lem3  15183  sylow3lem6  15186  efgval2  15276  efgsdm  15282  efgrelexlema  15301  efgcpbllemb  15307  iscyggen2  15411  cyggenod  15414  eldprd  15482  dprdf11  15501  dprddisj2  15517  pgpfac1lem2  15553  pgpfac1  15558  drngid2  15771  issubrg  15788  islmod  15874  aspval2  16325  psrbag  16351  zndvds  16746  znleval  16751  iunocv  16824  pjfval2  16852  pjdm2  16854  istopg  16884  istpsOLD  16901  basgen2  16970  isclo  17067  mretopd  17072  isnei  17083  isperf3  17132  restdis  17157  neitr  17159  restcls  17160  restlp  17162  restperf  17163  iscn  17214  iscnp  17216  lmbr2  17238  lmbrf  17239  ordtt1  17358  cmpsub  17378  hauscmplem  17384  cmpfi  17386  dfcon2  17396  1stcelcls  17438  1stccn  17440  nllyi  17452  subislly  17458  elkgen  17482  ptpjpre1  17517  ptuni2  17522  ptclsg  17561  ptcnplem  17567  txcn  17572  hausdiag  17591  txhaus  17593  txkgen  17598  xkoptsub  17600  cnmpt21  17617  elqtop  17643  tgqtop  17658  r0cld  17684  elfg  17817  fbasrn  17830  trfil2  17833  trfil3  17834  fin1aufil  17878  elfm2  17894  elfm3  17896  flimopn  17921  fbflim  17922  flfnei  17937  flftg  17942  cnpflf2  17946  txflf  17952  fclsbas  17967  alexsubALTlem4  17995  cnextfvval  18010  snclseqg  18059  tgphaus  18060  tsmsfbas  18071  tsmssubm  18086  utopsnneip  18192  prdsxmetlem  18299  imasdsf1olem  18304  xpsdsval  18312  blres  18344  isxms2  18361  metcnp  18454  txmetcnp  18460  txmetcn  18461  metustel  18463  metuel2  18478  dscopn  18485  isngp4  18522  cnblcld  18673  metnrmlem1a  18752  icoopnst  18828  iocopnst  18829  elpi1  18934  lmmbr2  19076  cfil3i  19086  caucfil  19100  iscmet3  19110  lmclim  19119  metcld2  19123  bcthlem4  19142  minveclem3b  19189  minveclem6  19195  minveclem7  19196  ivthle  19213  ivthle2  19214  evthicc2  19217  ovolfioo  19224  ovolficc  19225  ovolgelb  19236  dyadmax  19350  subopnmbl  19356  ismbf3d  19406  mbfimaopnlem  19407  mbfimaopn2  19409  mbfaddlem  19412  mbfsup  19416  mbfinf  19417  i1f1lem  19441  i1fmulclem  19454  itg1climres  19466  mbfi1fseqlem4  19470  itg2monolem1  19502  itg2gt0  19512  isibl  19517  iblcnlem1  19539  ellimc2  19624  dvcnvrelem1  19761  itgsubst  19793  mdegleb  19847  fta1glem2  19949  quotval  20069  vieta1lem1  20087  vieta1lem2  20088  ulm2  20161  ulmcaulem  20170  ulmcau  20171  radcnvlt1  20194  sineq0  20289  cos11  20295  recosf1o  20297  efopn  20409  cxpeq  20501  mcubic  20547  birthdaylem3  20652  rlimcnp  20664  xrlimcnp  20667  wilth  20714  isppw  20757  isppw2  20758  mumullem2  20823  sqff1o  20825  dvdsmulf1o  20839  fsumvma  20857  fsumvma2  20858  vmasum  20860  chpchtsum  20863  lgsne0  20977  lgseisenlem2  20994  lgsquadlem1  20998  lgsquadlem2  20999  dchrmusumlema  21047  rpvmasum2  21066  dchrisum0lema  21068  pntibndlem3  21146  pntlemi  21158  pntleml  21165  pnt3  21166  nbgraf1olem1  21310  nbgraf1olem5  21314  nbcusgra  21331  uvtx01vtx  21360  cusgrauvtxb  21364  iswlk  21384  istrl  21394  ispth  21415  isspth  21416  wlkdvspthlem  21448  usgrcyclnl2  21469  eupath2  21543  grpodiveq  21685  opidon  21751  issmgrp  21763  ismndo  21772  isrngo  21807  isdivrngo  21860  isvclem  21897  isnvlem  21930  isphg  22159  isph  22164  phoeqi  22200  ubthlem3  22215  minvecolem5  22224  minvecolem6  22225  minvecolem7  22226  hhph  22521  issh3  22563  nmopub  23252  nmfnleub  23269  adjeq  23279  adjvalval  23281  elunop2  23357  lnophm  23363  nmcexi  23370  cnlnadjlem5  23415  cnlnadjeui  23421  adjbd1o  23429  jpi  23614  mddmd2  23653  chrelati  23708  chrelat2i  23709  cvexchlem  23712  dmdbr5ati  23766  cdjreui  23776  cdj3i  23785  preqsnd  23837  abfmpunirn  23899  feqmptdf  23910  fmptcof2  23911  funcnvmptOLD  23916  funcnvmpt  23917  funcnv5mpt  23918  iocinioc2  23971  eliccioo  24009  xrmulc1cn  24113  isrrvv  24473  eldmgm  24578  dmgmaddn0  24579  lgamgulmlem6  24590  subfacp1lem3  24640  subfacp1lem6  24643  subfacp1  24644  txpcon  24691  sconpi1  24698  rescon  24705  cvmscbv  24717  cvmsval  24725  cvmlift2lem13  24774  cvmlift3lem2  24779  cvmlift3  24787  divelunit  24957  br8  25130  br6  25131  br4  25132  distel  25177  elpred  25194  poseq  25270  sltsolem1  25339  elfuns  25471  imageval  25486  funpartfv  25501  dfrdg4  25506  altopthg  25519  altopthbg  25520  brbtwn  25545  brcgr  25546  brbtwn2  25551  colinearalg  25556  axeuclidlem  25608  axcontlem2  25611  axcontlem4  25613  axcontlem7  25616  brcolinear2  25699  lineext  25717  brsegle  25749  seglelin  25757  broutsideof2  25763  bpolyval  25802  onsuct0  25898  supaddc  25940  supadd  25941  itg2addnclem2  25951  isfne4  26033  isfne2  26035  isfne3  26036  fneval  26051  topfneec  26055  neibastop2lem  26073  neibastop2  26074  neifg  26084  filnetlem4  26094  fdc  26133  heibor1  26203  rrncmslem  26225  rrnheibor  26230  isfldidl2  26363  isdmn3  26368  prtlem13  26401  prter3  26415  fnnfpeq0  26423  ralxpxfr2d  26425  ellz1  26509  lzunuz  26510  fz1eqin  26511  diophrex  26518  rexrabdioph  26538  rexfrabdioph  26539  2rexfrabdioph  26540  3rexfrabdioph  26541  4rexfrabdioph  26542  6rexfrabdioph  26543  7rexfrabdioph  26544  fzneg  26731  expdioph  26778  wepwsolem  26800  fnwe2lem2  26810  islmodfg  26829  kercvrlsm  26843  dsmmelbas  26867  ellspd  26916  islindf  26944  islindf4  26970  f1omvdconj  27051  sdrgacs  27171  pm10.52  27222  iotasbc  27281  pm14.122a  27284  pm14.122b  27285  pm14.123a  27287  rusbcALT  27301  fvsb  27316  stoweidlem34  27444  2reu4a  27628  sbcfun  27648  funressnfv  27654  dfafn5a  27686  frgra3vlem2  27747  frgrancvvdeqlem2  27776  frgrancvvdeqlem3  27777  frgrancvvdeqlemC  27784  gte-lte  27806  gt-lt  27807  bnj976  28479  bnj944  28640  bnj1173  28702  bnj1321  28727  bnj1373  28730  bnj1417  28741  ax12olem6NEW7  28790  sbcomwAUX7  28916  sbcomOLD7  29064  lrelat  29180  islshpat  29183  lshpsmreu  29275  lkrpssN  29329  cmtvalN  29377  omllaw2N  29410  cvrval  29435  cvrval2  29440  cvlsupr3  29510  3dim0  29622  islln2  29676  islpln5  29700  islpln2  29701  islpln2ah  29714  islvol5  29744  islvol2  29745  4atlem11  29774  pmapglbx  29934  cdleme18d  30460  cdlemefrs29bpre0  30561  cdlemb3  30771  cdlemg33b  30872  dvhb1dimN  31151  dia11N  31214  cdlemm10N  31284  dib11N  31326  dib1dim  31331  dibglbN  31332  diblsmopel  31337  dihopelvalcpre  31414  dih11  31431  dihmeetlem4preN  31472  dihmeetlem13N  31485  lcfrvalsnN  31707  lcfrlem9  31716  lcf1o  31717  mapdval4N  31798  baerlem3lem2  31876  baerlem5alem2  31877  baerlem5blem2  31878  hdmap1fval  31963  hdmapfval  31996  hdmapglem7a  32096  hlhillcs  32127
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
  Copyright terms: Public domain W3C validator