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

Theorem syl5ibr 236
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 213 . 2 (𝜒 → (𝜃𝜓))
41, 3syl5ib 234 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  syl5ibrcom  237  biimprd  238  exdistrf  2364  pm2.61ne  2908  unineq  3910  elpreqprlem  4426  oteqex  4993  elopabr  5042  otel3xp  5187  eqrelrdv2  5253  breldmg  5362  elrnmpt1  5406  cnveqb  5625  cnveq0  5626  predpoirr  5746  predfrirr  5747  ordtri3OLD  5798  limelon  5826  f1ssf1  6206  ndmfv  6256  ffvresb  6434  isomin  6627  isofrlem  6630  caovord3d  6886  eldifpw  7018  ssonuni  7028  onsucuni2  7076  ordzsl  7087  tfindsg  7102  findsg  7135  oteqimp  7229  frxp  7332  poxp  7334  fnwelem  7337  suppss  7370  wfrlem14  7473  tfrlem11  7529  oacl  7660  omcl  7661  oecl  7662  oa0r  7663  om0r  7664  om1r  7668  oe1m  7670  oaordi  7671  oawordri  7675  oaass  7686  oarec  7687  omwordri  7697  odi  7704  omass  7705  oewordri  7717  oeworde  7718  oeordsuc  7719  oelim2  7720  oeoa  7722  oeoelem  7723  oeoe  7724  nnm0r  7735  nnacl  7736  nnacom  7742  nnaordi  7743  nnaass  7747  nndi  7748  nnmass  7749  nnmsucr  7750  nnmcom  7751  omabs  7772  brecop  7883  eceqoveq  7895  elpm2r  7917  map0g  7939  undifixp  7986  fundmen  8071  mapxpen  8167  mapunen  8170  php  8185  unxpdomlem2  8206  pssnn  8219  f1vrnfibi  8292  elfir  8362  wemapso2lem  8498  wdompwdom  8524  inf3lem1  8563  inf3lem3  8565  cantnfval2  8604  cantnfp1lem3  8615  r1sdom  8675  r1tr  8677  carden2a  8830  fidomtri2  8858  prdom2  8867  infxpenlem  8874  acndom  8912  fodomacn  8917  wdomfil  8922  alephon  8930  alephordi  8935  alephle  8949  alephfplem3  8967  dfac2a  8990  kmlem9  9018  cflm  9110  cfslb  9126  cfslbn  9127  infpssrlem3  9165  infpssrlem4  9166  fin23lem21  9199  fin23lem30  9202  isf34lem7  9239  isf34lem6  9240  fin67  9255  isfin7-2  9256  fin1a2lem7  9266  fin1a2lem10  9269  iundom2g  9400  konigthlem  9428  alephreg  9442  gchdomtri  9489  wunr1om  9579  tskr1om  9627  inar1  9635  grur1a  9679  indpi  9767  genpprecl  9861  genpnmax  9867  addcmpblnr  9928  recexsrlem  9962  map2psrpr  9969  ax1rid  10020  axpre-mulgt0  10027  ltle  10164  nnmulcl  11081  nnsub  11097  nn0sub  11381  nneo  11499  uz11  11748  xrltle  12020  xltnegi  12085  xrsupsslem  12175  xrinfmsslem  12176  xrub  12180  supxrunb1  12187  supxrunb2  12188  om2uzuzi  12788  uzrdgxfr  12806  seqcl2  12859  seqfveq2  12863  seqshft2  12867  seqsplit  12874  seqcaopr3  12876  seqf1olem2a  12879  seqid2  12887  seqhomo  12888  ser1const  12897  m1expcl2  12922  expadd  12942  expmul  12945  faclbnd  13117  hashfzp1  13256  hashmap  13260  hashfacen  13276  hashf1lem1  13277  hashf1lem2  13278  hashf1  13279  seqcoll  13286  wrdsymb0  13371  len0nnbi  13373  swrdnd2  13479  wrd2ind  13523  swrdccatin12lem2  13535  swrdccatin1d  13545  repswccat  13578  repswcshw  13604  cshwcshid  13619  rtrclreclem3  13844  rtrclreclem4  13845  dfrtrcl2  13846  relexpindlem  13847  relexpind  13848  rtrclind  13849  recan  14120  rexanre  14130  rlimcn2  14365  caurcvg2  14452  fsumiun  14597  pwm1geoser  14644  efexp  14875  rpnnen2lem12  14998  dvdstr  15065  alzdvds  15089  zob  15130  sumeven  15157  sumodd  15158  bitsinv1  15211  smu01lem  15254  smupval  15257  smueqlem  15259  smumullem  15261  seq1st  15331  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  cncongr2  15429  prmdiveq  15538  odzdvds  15547  pythagtriplem2  15569  pcexp  15611  vdwlem13  15744  ramz  15776  prmolefac  15797  elrestr  16136  xpsff1o  16275  subsubc  16560  clatl  17163  frmdgsum  17446  dfgrp3e  17562  mulgneg2  17622  mulgnnass  17623  mulgnnassOLD  17624  mhmmulg  17630  gsumwrev  17842  symgbas  17846  symgextf1lem  17886  symgfixelsi  17901  pmtrdifellem4  17945  sylow1lem1  18059  efgsfo  18198  efgred  18207  cyggexb  18346  gsumzres  18356  gsum2dlem2  18416  ringadd2  18621  mulgass2  18647  lmodprop2d  18973  lspsnne2  19166  lspsneu  19171  assapropd  19375  mplcoe1  19513  mplcoe3  19514  mplcoe5  19516  ply1sclf1  19707  cnfldmulg  19826  cnfldexp  19827  zrhpsgnelbas  19988  mat1scmat  20393  restopn2  21029  cnpf2  21102  cmpfi  21259  txcn  21477  txlm  21499  xkoptsub  21505  xkopjcn  21507  ufildr  21782  cnflf  21853  fclsnei  21870  fclscmp  21881  ufilcmp  21883  cnfcf  21893  symgtgp  21952  isxms2  22300  met2ndc  22375  metustbl  22418  tngngp2  22503  clmmulg  22947  iscau4  23123  ovolunlem1a  23310  ovolicc2lem4  23334  volfiniun  23361  voliunlem1  23364  volsup  23370  dvnadd  23737  dvnres  23739  dvcobr  23754  ply1nzb  23927  plypf1  24013  dgrle  24044  coeaddlem  24050  dgrlt  24067  dvntaylp  24170  cxpmul2  24480  rlimcnp  24737  facgam  24837  wilthlem2  24840  isnsqf  24906  musum  24962  chtub  24982  chpval2  24988  gausslemma2dlem0i  25134  dchrisumlem1  25223  qabvexp  25360  ostthlem2  25362  axsegconlem1  25842  ax5seglem4  25857  ax5seglem5  25858  axlowdimlem15  25881  axcontlem2  25890  axcontlem4  25892  incistruhgr  26019  upgredg2vtx  26081  upgredgpr  26082  numedglnl  26084  uhgr2edg  26145  nbupgruvtxres  26358  cusgrfilem1  26407  wlkres  26623  wlkp1lem2  26627  pthdivtx  26681  pthdlem2lem  26719  wlkiswwlks2lem4  26826  wwlksnredwwlkn0  26859  wwlksnextwrd  26860  wwlksnextprop  26875  clwlkclwwlklem2a  26964  erclwwlksym  26978  clwwlkf1  27012  eleclclwwlknlem2  27026  erclwwlknsym  27034  clwwlknonex2  27084  eupth2lem3lem6  27211  frgr3vlem1  27253  3vfriswmgrlem  27257  2clwwlk2clwwlklem2lem2  27329  extwwlkfab  27342  sspval  27706  nmosetre  27747  nmobndseqi  27762  nmobndseqiALT  27763  orthcom  28093  shsva  28307  shmodsi  28376  h1datomi  28568  nmopsetretALT  28850  nmfnsetre  28864  lnopcnbd  29023  pjclem4  29186  pj3si  29194  ssmd1  29298  atom1d  29340  chjatom  29344  atcvat4i  29384  cdj3lem2a  29423  cdj3lem3a  29426  disjunsn  29533  unitdivcld  30075  xrge0iifiso  30109  dya2iocuni  30473  bnj168  30924  bnj535  31086  bnj590  31106  bnj594  31108  bnj938  31133  bnj1118  31178  bnj1128  31184  deranglem  31274  subfacp1lem6  31293  subfacval2  31295  cvmlift2lem12  31422  mrsubvrs  31545  msrrcl  31566  mclsax  31592  dfon2lem6  31817  rdgprc  31824  trpredlem1  31851  frrlem5e  31913  nodenselem8  31966  slerec  32048  ifscgr  32276  btwncolinear1  32301  hfelhf  32413  opnrebl2  32441  nn0prpw  32443  ordcmp  32571  findreccl  32577  nndivlub  32582  bj-rest0  33171  topdifinffinlem  33325  iooelexlt  33340  rdgeqoa  33348  wl-mo3t  33488  matunitlindflem2  33536  poimirlem2  33541  poimirlem23  33562  poimirlem28  33567  poimirlem29  33568  poimirlem31  33570  poimirlem32  33571  eqfnun  33646  sdclem2  33668  sdclem1  33669  prdsbnd2  33724  ismtyval  33729  rrnequiv  33764  isexid2  33784  ismndo1  33802  exidreslem  33806  rngo2  33836  rngoueqz  33869  risci  33916  prtlem11  34470  prtlem15  34479  cvrat4  35047  lcfl6  37106  clcnvlem  38247  cnvrcl0  38249  cnvtrcl0  38250  iunrelexpmin1  38317  iunrelexpmin2  38321  aovmpt4g  41602  iccpartiltu  41683  iccpartgt  41688  iccpartgel  41690  pfxccatin12lem2  41749  fmtnofac1  41807  gbepos  41971  funcrngcsetc  42323  funcrngcsetcALT  42324  rhmsscrnghm  42351  funcringcsetc  42360  ellcoellss  42549  dignn0flhalflem2  42735  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator