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  2466  pm2.61ne  3106  unineq  4257  elpreqprlem  4794  oteqex  5386  elopabr  5443  otel3xp  5597  eqrelrdv2  5666  breldmg  5776  elrnmpt1  5828  cnveqb  6050  cnveq0  6051  predpoirr  6173  predfrirr  6174  limelon  6251  f1ssf1  6642  ndmfv  6696  ffvresb  6883  isomin  7085  isofrlem  7088  oprabidw  7182  caovord3d  7351  eldifpw  7482  ssonuni  7492  onsucuni2  7540  ordzsl  7551  tfindsg  7566  findsg  7600  oteqimp  7702  frxp  7814  poxp  7816  fnwelem  7819  suppss  7854  wfrlem14  7962  tfrlem11  8018  oacl  8154  omcl  8155  oecl  8156  oa0r  8157  om0r  8158  om1r  8162  oe1m  8164  oaordi  8165  oawordri  8169  oaass  8180  oarec  8181  omwordri  8191  odi  8198  omass  8199  oewordri  8211  oeworde  8212  oeordsuc  8213  oelim2  8214  oeoa  8216  oeoelem  8217  oeoe  8218  nnm0r  8229  nnacl  8230  nnacom  8236  nnaordi  8237  nnaass  8241  nndi  8242  nnmass  8243  nnmsucr  8244  nnmcom  8245  omabs  8267  brecop  8383  eceqoveq  8395  elpm2r  8417  map0g  8441  undifixp  8490  fundmen  8575  mapxpen  8675  mapunen  8678  php  8693  unxpdomlem2  8715  pssnn  8728  f1vrnfibi  8801  elfir  8871  wemapso2lem  9008  wdompwdom  9034  inf3lem1  9083  inf3lem3  9085  cantnfval2  9124  cantnfp1lem3  9135  r1sdom  9195  r1tr  9197  carden2a  9387  fidomtri2  9415  prdom2  9424  infxpenlem  9431  acndom  9469  fodomacn  9474  wdomfil  9479  alephon  9487  alephordi  9492  alephle  9506  alephfplem3  9524  dfac2a  9547  kmlem9  9576  cflm  9664  cfslb  9680  cfslbn  9681  infpssrlem3  9719  infpssrlem4  9720  fin23lem21  9753  fin23lem30  9756  isf34lem7  9793  isf34lem6  9794  fin67  9809  isfin7-2  9810  fin1a2lem7  9820  fin1a2lem10  9823  iundom2g  9954  konigthlem  9982  alephreg  9996  gchdomtri  10043  wunr1om  10133  tskr1om  10181  inar1  10189  grur1a  10233  indpi  10321  genpprecl  10415  genpnmax  10421  addcmpblnr  10483  recexsrlem  10517  map2psrpr  10524  ax1rid  10575  axpre-mulgt0  10582  ltle  10721  nnmulcl  11653  nnsub  11673  nn0sub  11939  nneo  12058  uz11  12259  xrltle  12535  xltnegi  12602  xrsupsslem  12693  xrinfmsslem  12694  xrub  12698  supxrunb1  12705  supxrunb2  12706  om2uzuzi  13310  uzrdgxfr  13328  seqcl2  13381  seqfveq2  13385  seqshft2  13389  seqsplit  13396  seqcaopr3  13398  seqf1olem2a  13401  seqid2  13409  seqhomo  13410  ser1const  13419  m1expcl2  13444  expadd  13464  expmul  13467  faclbnd  13643  hashfzp1  13785  hashmap  13789  hashfacen  13805  hashf1lem1  13806  hashf1lem2  13807  hashf1  13808  seqcoll  13815  wrdsymb0  13894  len0nnbi  13896  eqs1  13959  swrdnd2  14010  wrd2ind  14078  pfxccatin12lem2c  14085  pfxccatin12lem2  14086  swrdccatin1d  14098  repswccat  14141  repswcshw  14167  cshwcshid  14182  rtrclreclem3  14412  rtrclreclem4  14413  dfrtrcl2  14414  relexpindlem  14415  relexpind  14416  rtrclind  14417  recan  14689  rexanre  14699  rlimcn2  14940  caurcvg2  15027  fsumiun  15168  pwm1geoserOLD  15217  efexp  15446  rpnnen2lem12  15570  dvdstr  15638  alzdvds  15662  zob  15700  sumeven  15730  sumodd  15731  bitsinv1  15783  smu01lem  15826  smupval  15829  smueqlem  15831  smumullem  15833  seq1st  15907  lcmfunsnlem2lem1  15974  lcmfunsnlem2lem2  15975  cncongr2  16004  prmdiveq  16115  odzdvds  16124  pythagtriplem2  16146  pcexp  16188  vdwlem13  16321  ramz  16353  prmolefac  16374  elrestr  16694  xpsff1o  16832  subsubc  17115  clatl  17718  frmdgsum  18012  dfgrp3e  18131  mulgneg2  18193  mulgnnass  18194  mhmmulg  18200  gsumwrev  18426  symgbas  18430  symgextf1lem  18470  symgfixelsi  18485  pmtrdifellem4  18529  sylow1lem1  18645  efgsfo  18787  efgred  18796  cyggexb  18941  gsumzres  18951  gsum2dlem2  19013  ringadd2  19247  mulgass2  19273  lmodprop2d  19618  lspsnne2  19812  lspsneu  19817  assapropd  20022  mplcoe1  20166  mplcoe3  20167  mplcoe5  20169  ply1sclf1  20374  cnfldmulg  20493  cnfldexp  20494  zrhpsgnelbas  20654  mat1scmat  21064  restopn2  21701  cnpf2  21774  cmpfi  21932  txcn  22150  txlm  22172  xkoptsub  22178  xkopjcn  22180  ufildr  22455  cnflf  22526  fclsnei  22543  fclscmp  22554  ufilcmp  22556  cnfcf  22566  symgtgp  22625  isxms2  22973  met2ndc  23048  metustbl  23091  tngngp2  23176  clmmulg  23620  iscau4  23797  ovolunlem1a  24012  ovolicc2lem4  24036  volfiniun  24063  voliunlem1  24066  volsup  24072  dvnadd  24441  dvnres  24443  dvcobr  24458  ply1nzb  24631  plypf1  24717  dgrle  24748  coeaddlem  24754  dgrlt  24771  dvntaylp  24874  cxpmul2  25185  rlimcnp  25457  facgam  25557  wilthlem2  25560  isnsqf  25626  musum  25682  chtub  25702  chpval2  25708  gausslemma2dlem0i  25854  dchrisumlem1  25979  qabvexp  26116  ostthlem2  26118  axsegconlem1  26617  ax5seglem4  26632  ax5seglem5  26633  axlowdimlem15  26656  axcontlem2  26665  axcontlem4  26667  incistruhgr  26778  upgredg2vtx  26840  upgredgpr  26841  numedglnl  26843  uhgr2edg  26904  nbupgruvtxres  27103  cusgrfilem1  27151  wlkres  27366  wlkp1lem2  27370  pthdivtx  27424  pthdlem2lem  27462  wlkiswwlks2lem4  27564  wwlksnredwwlkn0  27588  wwlksnextwrd  27589  wwlksnfi  27598  wwlksnextprop  27605  clwlkclwwlklem2a  27690  clwlkclwwlkf1lem2  27697  erclwwlksym  27713  clwwlkf1  27742  eleclclwwlknlem2  27754  erclwwlknsym  27763  clwwlknonex2  27802  eupth2lem3lem6  27926  frgr3vlem1  27966  3vfriswmgrlem  27970  wlkl0  28060  sspval  28414  nmosetre  28455  nmobndseqi  28470  nmobndseqiALT  28471  orthcom  28799  shsva  29011  shmodsi  29080  h1datomi  29272  nmopsetretALT  29554  nmfnsetre  29568  lnopcnbd  29727  pjclem4  29890  pj3si  29898  ssmd1  30002  atom1d  30044  chjatom  30048  atcvat4i  30088  cdj3lem2a  30127  cdj3lem3a  30130  disjunsn  30259  unitdivcld  31030  xrge0iifiso  31064  dya2iocuni  31427  bnj168  31886  bnj535  32048  bnj590  32068  bnj594  32070  bnj938  32095  bnj1118  32140  bnj1128  32146  deranglem  32297  subfacp1lem6  32316  subfacval2  32318  cvmlift2lem12  32445  satffun  32540  mrsubvrs  32653  msrrcl  32674  mclsax  32700  dfon2lem6  32917  rdgprc  32923  trpredlem1  32950  nodenselem8  33079  slerec  33161  ifscgr  33389  btwncolinear1  33414  hfelhf  33526  opnrebl2  33553  nn0prpw  33555  ordcmp  33679  findreccl  33685  nndivlub  33690  bj-rest0  34265  bj-isrvec2  34456  topdifinffinlem  34497  iooelexlt  34512  rdgeqoa  34520  exrecfnlem  34529  wl-mo3t  34679  matunitlindflem2  34756  poimirlem2  34761  poimirlem23  34782  poimirlem28  34787  poimirlem29  34788  poimirlem31  34790  poimirlem32  34791  eqfnun  34865  sdclem2  34885  sdclem1  34886  prdsbnd2  34941  ismtyval  34946  rrnequiv  34981  isexid2  35001  ismndo1  35019  exidreslem  35023  rngo2  35053  rngoueqz  35086  risci  35133  prtlem11  35869  prtlem15  35878  cvrat4  36446  lcfl6  38503  harval3  39765  clcnvlem  39844  cnvrcl0  39846  cnvtrcl0  39847  iunrelexpmin1  39914  iunrelexpmin2  39918  aovmpt4g  43262  iccpartiltu  43410  iccpartgt  43415  iccpartgel  43417  reuopreuprim  43516  fmtnofac1  43560  gbepos  43751  funcrngcsetc  44097  funcrngcsetcALT  44098  rhmsscrnghm  44125  funcringcsetc  44134  ellcoellss  44318  dignn0flhalflem2  44504  nn0sumshdiglemB  44508
  Copyright terms: Public domain W3C validator