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

Theorem syl5ibr 225
Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)
Hypotheses
Ref Expression
syl5ibr.1  |-  ( ph  ->  th )
syl5ibr.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ibr  |-  ( ch 
->  ( ph  ->  ps ) )

Proof of Theorem syl5ibr
StepHypRef Expression
1 syl5ibr.1 . 2  |-  ( ph  ->  th )
2 syl5ibr.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
32bicomd 205 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 223 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189
This theorem is referenced by:  syl5ibrcom  226  biimprd  227  exdistrf  2131  pm2.61ne  2740  pm2.61neOLD  2741  unineq  3724  oteqex  4711  otel3xp  4887  elrnmpt1  5100  cnveqb  5308  cnveq0  5309  relcoi1OLD  5382  predpoirr  5425  predfrirr  5426  ordtri3  5476  limelon  5503  ndmfv  5903  ffvresb  6067  isomin  6241  isofrlem  6244  caovord3d  6491  eldifpw  6615  ssonuni  6625  onsucuni2  6673  ordzsl  6684  tfindsg  6699  findsg  6732  oteqimp  6824  frxp  6915  poxp  6917  fnwelem  6920  suppss  6954  wfrlem14  7055  tfrlem11  7112  oacl  7243  omcl  7244  oecl  7245  oa0r  7246  om0r  7247  om1r  7250  oe1m  7252  oaordi  7253  oawordri  7257  oaass  7268  oarec  7269  omwordri  7279  odi  7286  omass  7287  oewordri  7299  oeworde  7300  oeordsuc  7301  oelim2  7302  oeoa  7304  oeoelem  7305  oeoe  7306  nnm0r  7317  nnacl  7318  nnacom  7324  nnaordi  7325  nnaass  7329  nndi  7330  nnmass  7331  nnmsucr  7332  nnmcom  7333  omabs  7354  brecop  7462  eceqoveq  7474  elpm2r  7495  map0g  7517  undifixp  7564  fundmen  7648  mapxpen  7742  mapunen  7745  php  7760  unxpdomlem2  7781  pssnn  7794  f1vrnfibi  7863  elfir  7933  wemapso2lem  8071  wdompwdom  8097  inf3lem1  8137  inf3lem3  8139  cantnfval2  8177  cantnfp1lem3  8188  r1sdom  8248  r1tr  8250  carden2a  8403  fidomtri2  8431  prdom2  8440  infxpenlem  8447  acndom  8484  fodomacn  8489  wdomfil  8494  alephon  8502  alephordi  8507  alephle  8521  alephfplem3  8539  dfac2a  8562  kmlem9  8590  cflm  8682  cfslb  8698  cfslbn  8699  infpssrlem3  8737  infpssrlem4  8738  fin23lem21  8771  fin23lem30  8774  isf34lem7  8811  isf34lem6  8812  fin67  8827  isfin7-2  8828  fin1a2lem7  8838  fin1a2lem10  8841  iundom2g  8967  konigthlem  8995  alephreg  9009  gchdomtri  9056  wunr1om  9146  tskr1om  9194  inar1  9202  grur1a  9246  indpi  9334  genpprecl  9428  genpnmax  9434  addcmpblnr  9495  recexsrlem  9529  map2psrpr  9536  ax1rid  9587  axpre-mulgt0  9594  ltle  9724  nnmulcl  10634  nnsub  10650  nn0sub  10922  nneo  11021  uz11  11183  xrltle  11450  xltnegi  11511  xrsupsslem  11594  xrinfmsslem  11595  xrub  11599  supxrunb1  11607  supxrunb2  11608  om2uzuzi  12164  uzrdgxfr  12181  seqcl2  12232  seqfveq2  12236  seqshft2  12240  seqsplit  12247  seqcaopr3  12249  seqf1olem2a  12252  seqid2  12260  seqhomo  12261  ser1const  12270  m1expcl2  12295  expadd  12315  expmul  12318  faclbnd  12476  hashmap  12606  hashfacen  12616  hashf1lem1  12617  hashf1lem2  12618  hashf1  12619  seqcoll  12626  wrdsymb0  12699  swrdnd2  12785  wrd2ind  12830  swrdccatin12lem2  12841  swrdccatin1d  12851  repswccat  12884  repswcshw  12907  cshwcshid  12922  rtrclreclem3  13117  rtrclreclem4  13118  dfrtrcl2  13119  relexpindlem  13120  relexpind  13121  rtrclind  13122  recan  13393  rexanre  13403  rlimcn2  13647  caurcvg2  13737  fsumiun  13874  efexp  14148  rpnnen2  14271  dvdstr  14330  alzdvds  14348  bitsinv1  14409  smu01lem  14452  smupval  14455  smueqlem  14457  smumullem  14459  seq1st  14523  lcmfunsnlem2lem1  14604  lcmfunsnlem2lem2  14605  prmdiveq  14727  odzdvds  14733  odzdvdsOLD  14739  pythagtriplem2  14760  pcexp  14802  vdwlem13  14936  ramz  14976  prmolefac  14997  prmorlefacOLD  15011  elrestr  15320  xpsff1o  15467  subsubc  15751  clatl  16355  frmdgsum  16639  mulgneg2  16778  mulgnnass  16779  mhmmulg  16783  gsumwrev  17010  symgbas  17014  symgextf1lem  17054  symgfixelsi  17069  pmtrdifellem4  17113  sylow1lem1  17243  efgsfo  17382  efgred  17391  cyggexb  17526  gsumzres  17536  gsum2dlem2  17596  mulgass2  17822  lmodprop2d  18143  lspsnne2  18334  lspsneu  18339  assapropd  18544  mplcoe1  18682  mplcoe3  18683  mplcoe5  18685  ply1sclf1  18875  cnfldmulg  18993  cnfldexp  18994  zrhpsgnelbas  19154  mat1scmat  19556  restopn2  20185  cnpf2  20258  cmpfi  20415  txcn  20633  txlm  20655  xkoptsub  20661  xkopjcn  20663  ufildr  20938  cnflf  21009  fclsnei  21026  fclscmp  21037  ufilcmp  21039  cnfcf  21049  symgtgp  21108  isxms2  21455  met2ndc  21530  metustbl  21573  tngngp2  21652  clmmulg  22116  iscau4  22241  ovolunlem1a  22441  ovolicc2lem4OLD  22465  ovolicc2lem4  22466  volfiniun  22492  voliunlem1  22495  volsup  22501  dvnadd  22875  dvnres  22877  dvcobr  22892  ply1nzb  23063  plypf1  23158  dgrle  23189  coeaddlem  23195  dgrlt  23212  dvntaylp  23318  cxpmul2  23626  rlimcnp  23883  facgam  23983  wilthlem2  23986  isnsqf  24054  musum  24112  chtub  24132  chpval2  24138  dchrisumlem1  24319  qabvexp  24456  ostthlem2  24458  axsegconlem1  24939  ax5seglem4  24954  ax5seglem5  24955  axlowdimlem15  24978  axcontlem2  24987  axcontlem4  24989  ushgrauhgra  25022  usgra2edg  25101  cusgrafilem1  25199  sizeusglecusglem1  25204  sizeusglecusg  25206  trliswlk  25261  2trllemF  25271  constr3lem6  25369  1conngra  25395  wlkiswwlk2lem4  25414  wwlknredwwlkn0  25447  wwlkextwrd  25448  wwlkextproplem1  25461  wwlkextprop  25464  clwlkisclwwlklem2a  25505  clwwlkf1  25516  erclwwlksym  25534  eleclclwwlknlem2  25538  erclwwlknsym  25546  el2wlkonot  25589  el2spthonot  25590  hashnbgravdg  25633  eupatrl  25688  frgra3vlem1  25720  3vfriswmgralem  25724  frconngra  25741  frgrawopreglem3  25766  frg2wot1  25777  2spotiundisj  25782  usg2spot2nb  25785  usgreg2spot  25787  extwwlkfablem2  25798  numclwwlkovf2ex  25806  extwwlkfab  25810  isexid2  26045  ismndo1  26064  rngo2  26108  rngoueqz  26150  sspval  26354  nmosetre  26397  nmobndseqi  26412  nmobndseqiALT  26413  orthcom  26753  shsva  26965  shmodsi  27034  h1datomi  27226  nmopsetretALT  27508  nmfnsetre  27522  lnopcnbd  27681  pjclem4  27844  pj3si  27852  ssmd1  27956  atom1d  27998  chjatom  28002  atcvat4i  28042  cdj3lem2a  28081  cdj3lem3a  28084  disjunsn  28200  unitdivcld  28709  xrge0iifiso  28743  dya2iocuni  29107  bnj168  29540  bnj535  29703  bnj590  29723  bnj594  29725  bnj938  29750  bnj1118  29795  bnj1128  29801  deranglem  29891  subfacp1lem6  29910  subfacval2  29912  cvmlift2lem12  30039  mrsubvrs  30162  msrrcl  30183  mclsax  30209  dfon2lem6  30435  rdgprc  30442  trpredlem1  30469  frrlem5e  30523  nodenselem8  30576  ifscgr  30810  btwncolinear1  30835  hfelhf  30947  opnrebl2  30976  nn0prpw  30978  ordcmp  31106  findreccl  31112  nndivlub  31117  topdifinffinlem  31697  iooelexlt  31712  wl-mo3t  31825  poimirlem2  31862  poimirlem23  31883  poimirlem28  31888  poimirlem29  31889  poimirlem31  31891  poimirlem32  31892  eqfnun  31968  sdclem2  31991  sdclem1  31992  prdsbnd2  32047  ismtyval  32052  rrnequiv  32087  exidreslem  32095  risci  32146  prtlem11  32362  prtlem15  32371  cvrat4  32933  lcfl6  34993  iunrelexpmin1  36166  iunrelexpmin2  36170  aovmpt4g  38421  iccpartiltu  38454  iccpartgt  38459  iccpartgel  38461  zob  38481  gbepos  38577  pfxccatin12lem2  38683  usgr2edg  38916  ushguhg  38987  funcrngcsetc  39304  funcrngcsetcALT  39305  rhmsscrnghm  39332  funcringcsetc  39341  ellcoellss  39534  dignn0flhalflem2  39733  nn0sumshdiglemB  39737
  Copyright terms: Public domain W3C validator