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

Theorem syl5ibr 247
Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)
Hypotheses
Ref Expression
syl5ibr.1 (𝜑𝜃)
syl5ibr.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5ibr (𝜒 → (𝜑𝜓))

Proof of Theorem syl5ibr
StepHypRef Expression
1 syl5ibr.1 . 2 (𝜑𝜃)
2 syl5ibr.2 . . 3 (𝜒 → (𝜓𝜃))
32bicomd 224 . 2 (𝜒 → (𝜃𝜓))
41, 3syl5ib 245 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  syl5ibrcom  248  biimprd  249  exdistrf  2464  pm2.61ne  3102  unineq  4253  elpreqprlem  4790  oteqex  5382  elopabr  5439  otel3xp  5593  eqrelrdv2  5662  breldmg  5772  elrnmpt1  5824  cnveqb  6047  cnveq0  6048  predpoirr  6170  predfrirr  6171  limelon  6248  f1ssf1  6640  ndmfv  6694  ffvresb  6881  isomin  7079  isofrlem  7082  oprabidw  7176  caovord3d  7347  eldifpw  7478  ssonuni  7489  onsucuni2  7537  ordzsl  7548  tfindsg  7563  findsg  7597  oteqimp  7699  frxp  7811  poxp  7813  fnwelem  7816  suppss  7851  wfrlem14  7959  tfrlem11  8015  oacl  8151  omcl  8152  oecl  8153  oa0r  8154  om0r  8155  om1r  8159  oe1m  8161  oaordi  8162  oawordri  8166  oaass  8177  oarec  8178  omwordri  8188  odi  8195  omass  8196  oewordri  8208  oeworde  8209  oeordsuc  8210  oelim2  8211  oeoa  8213  oeoelem  8214  oeoe  8215  nnm0r  8226  nnacl  8227  nnacom  8233  nnaordi  8234  nnaass  8238  nndi  8239  nnmass  8240  nnmsucr  8241  nnmcom  8242  omabs  8264  brecop  8380  eceqoveq  8392  elpm2r  8414  map0g  8438  undifixp  8487  fundmen  8572  mapxpen  8672  mapunen  8675  php  8690  unxpdomlem2  8712  pssnn  8725  f1vrnfibi  8798  elfir  8868  wemapso2lem  9005  wdompwdom  9031  inf3lem1  9080  inf3lem3  9082  cantnfval2  9121  cantnfp1lem3  9132  r1sdom  9192  r1tr  9194  carden2a  9384  fidomtri2  9412  prdom2  9421  infxpenlem  9428  acndom  9466  fodomacn  9471  wdomfil  9476  alephon  9484  alephordi  9489  alephle  9503  alephfplem3  9521  dfac2a  9544  kmlem9  9573  cflm  9661  cfslb  9677  cfslbn  9678  infpssrlem3  9716  infpssrlem4  9717  fin23lem21  9750  fin23lem30  9753  isf34lem7  9790  isf34lem6  9791  fin67  9806  isfin7-2  9807  fin1a2lem7  9817  fin1a2lem10  9820  iundom2g  9951  konigthlem  9979  alephreg  9993  gchdomtri  10040  wunr1om  10130  tskr1om  10178  inar1  10186  grur1a  10230  indpi  10318  genpprecl  10412  genpnmax  10418  addcmpblnr  10480  recexsrlem  10514  map2psrpr  10521  ax1rid  10572  axpre-mulgt0  10579  ltle  10718  nnmulcl  11650  nnsub  11670  nn0sub  11936  nneo  12055  uz11  12256  xrltle  12532  xltnegi  12599  xrsupsslem  12690  xrinfmsslem  12691  xrub  12695  supxrunb1  12702  supxrunb2  12703  om2uzuzi  13307  uzrdgxfr  13325  seqcl2  13378  seqfveq2  13382  seqshft2  13386  seqsplit  13393  seqcaopr3  13395  seqf1olem2a  13398  seqid2  13406  seqhomo  13407  ser1const  13416  m1expcl2  13441  expadd  13461  expmul  13464  faclbnd  13640  hashfzp1  13782  hashmap  13786  hashfacen  13802  hashf1lem1  13803  hashf1lem2  13804  hashf1  13805  seqcoll  13812  wrdsymb0  13891  len0nnbi  13893  eqs1  13956  swrdnd2  14007  wrd2ind  14075  pfxccatin12lem2c  14082  pfxccatin12lem2  14083  swrdccatin1d  14095  repswccat  14138  repswcshw  14164  cshwcshid  14179  rtrclreclem3  14409  rtrclreclem4  14410  dfrtrcl2  14411  relexpindlem  14412  relexpind  14413  rtrclind  14414  recan  14686  rexanre  14696  rlimcn2  14937  caurcvg2  15024  fsumiun  15166  pwm1geoserOLD  15215  efexp  15444  rpnnen2lem12  15568  dvdstr  15636  alzdvds  15660  zob  15698  sumeven  15728  sumodd  15729  bitsinv1  15781  smu01lem  15824  smupval  15827  smueqlem  15829  smumullem  15831  seq1st  15905  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  cncongr2  16002  prmdiveq  16113  odzdvds  16122  pythagtriplem2  16144  pcexp  16186  vdwlem13  16319  ramz  16351  prmolefac  16372  elrestr  16692  xpsff1o  16830  subsubc  17113  clatl  17716  frmdgsum  18017  dfgrp3e  18139  mulgneg2  18201  mulgnnass  18202  mhmmulg  18208  gsumwrev  18434  symgbas  18438  symgextf1lem  18479  symgfixelsi  18494  pmtrdifellem4  18538  sylow1lem1  18654  efgsfo  18796  efgred  18805  cyggexb  18950  gsumzres  18960  gsum2dlem2  19022  ringadd2  19256  mulgass2  19282  lmodprop2d  19627  lspsnne2  19821  lspsneu  19826  assapropd  20031  mplcoe1  20176  mplcoe3  20177  mplcoe5  20179  ply1sclf1  20387  cnfldmulg  20507  cnfldexp  20508  zrhpsgnelbas  20668  mat1scmat  21078  restopn2  21715  cnpf2  21788  cmpfi  21946  txcn  22164  txlm  22186  xkoptsub  22192  xkopjcn  22194  ufildr  22469  cnflf  22540  fclsnei  22557  fclscmp  22568  ufilcmp  22570  cnfcf  22580  symgtgp  22639  isxms2  22987  met2ndc  23062  metustbl  23105  tngngp2  23190  clmmulg  23634  iscau4  23811  ovolunlem1a  24026  ovolicc2lem4  24050  volfiniun  24077  voliunlem1  24080  volsup  24086  dvnadd  24455  dvnres  24457  dvcobr  24472  ply1nzb  24645  plypf1  24731  dgrle  24762  coeaddlem  24768  dgrlt  24785  dvntaylp  24888  cxpmul2  25199  rlimcnp  25471  facgam  25571  wilthlem2  25574  isnsqf  25640  musum  25696  chtub  25716  chpval2  25722  gausslemma2dlem0i  25868  dchrisumlem1  25993  qabvexp  26130  ostthlem2  26132  axsegconlem1  26631  ax5seglem4  26646  ax5seglem5  26647  axlowdimlem15  26670  axcontlem2  26679  axcontlem4  26681  incistruhgr  26792  upgredg2vtx  26854  upgredgpr  26855  numedglnl  26857  uhgr2edg  26918  nbupgruvtxres  27117  cusgrfilem1  27165  wlkres  27380  wlkp1lem2  27384  pthdivtx  27438  pthdlem2lem  27476  wlkiswwlks2lem4  27578  wwlksnredwwlkn0  27602  wwlksnextwrd  27603  wwlksnfi  27612  wwlksnextprop  27619  clwlkclwwlklem2a  27704  clwlkclwwlkf1lem2  27711  erclwwlksym  27727  clwwlkf1  27756  eleclclwwlknlem2  27768  erclwwlknsym  27777  clwwlknonex2  27816  eupth2lem3lem6  27940  frgr3vlem1  27980  3vfriswmgrlem  27984  wlkl0  28074  sspval  28428  nmosetre  28469  nmobndseqi  28484  nmobndseqiALT  28485  orthcom  28813  shsva  29025  shmodsi  29094  h1datomi  29286  nmopsetretALT  29568  nmfnsetre  29582  lnopcnbd  29741  pjclem4  29904  pj3si  29912  ssmd1  30016  atom1d  30058  chjatom  30062  atcvat4i  30102  cdj3lem2a  30141  cdj3lem3a  30144  disjunsn  30273  unitdivcld  31044  xrge0iifiso  31078  dya2iocuni  31441  bnj168  31900  bnj535  32062  bnj590  32082  bnj594  32084  bnj938  32109  bnj1118  32154  bnj1128  32160  deranglem  32311  subfacp1lem6  32330  subfacval2  32332  cvmlift2lem12  32459  satffun  32554  mrsubvrs  32667  msrrcl  32688  mclsax  32714  dfon2lem6  32931  rdgprc  32937  trpredlem1  32964  nodenselem8  33093  slerec  33175  ifscgr  33403  btwncolinear1  33428  hfelhf  33540  opnrebl2  33567  nn0prpw  33569  ordcmp  33693  findreccl  33699  nndivlub  33704  bj-rest0  34279  bj-isrvec2  34470  topdifinffinlem  34511  iooelexlt  34526  rdgeqoa  34534  exrecfnlem  34543  wl-mo3t  34694  matunitlindflem2  34771  poimirlem2  34776  poimirlem23  34797  poimirlem28  34802  poimirlem29  34803  poimirlem31  34805  poimirlem32  34806  eqfnun  34880  sdclem2  34900  sdclem1  34901  prdsbnd2  34956  ismtyval  34961  rrnequiv  34996  isexid2  35016  ismndo1  35034  exidreslem  35038  rngo2  35068  rngoueqz  35101  risci  35148  prtlem11  35884  prtlem15  35893  cvrat4  36461  lcfl6  38518  harval3  39784  clcnvlem  39863  cnvrcl0  39865  cnvtrcl0  39866  iunrelexpmin1  39933  iunrelexpmin2  39937  aovmpt4g  43281  iccpartiltu  43429  iccpartgt  43434  iccpartgel  43436  reuopreuprim  43535  fmtnofac1  43579  gbepos  43770  sursubmefmnd  43963  injsubmefmnd  43964  symgsubmefmndALT  43966  smndex1mndlem  43979  funcrngcsetc  44167  funcrngcsetcALT  44168  rhmsscrnghm  44195  funcringcsetc  44204  ellcoellss  44388  dignn0flhalflem2  44574  nn0sumshdiglemB  44578
  Copyright terms: Public domain W3C validator