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

Theorem syl5ibrcom 237
Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)
Hypotheses
Ref Expression
syl5ibr.1 (𝜑𝜃)
syl5ibr.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5ibrcom (𝜑 → (𝜒𝜓))

Proof of Theorem syl5ibrcom
StepHypRef Expression
1 syl5ibr.1 . . 3 (𝜑𝜃)
2 syl5ibr.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2syl5ibr 236 . 2 (𝜒 → (𝜑𝜓))
43com12 32 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:  biimprcd  240  elsn2g  4201  preq1b  4368  elpreqprb  4388  reusv2lem2OLD  4861  reusv3  4867  alxfr  4869  reuhypd  4886  opth1  4934  euotd  4965  otiunsndisj  4970  tz7.2  5088  frsn  5179  elsnxp  5665  ordtri1  5744  ordtri3  5747  fvmptdv2  6284  fveqressseq  6341  foco2  6365  foco2OLD  6366  fsn  6387  fnsnb  6417  fmptsng  6419  fmptsnd  6420  fconst2g  6453  fnprb  6457  fntpb  6458  funfvima  6477  soisoi  6563  isores3  6570  riotaeqimp  6619  eusvobj2  6628  ovmpt2dv2  6779  f1opw2  6873  sorpssun  6929  sorpssin  6930  oneqmin  6990  nlimsucg  7027  onzsl  7031  tfinds  7044  funcnvuni  7104  opiota  7214  mpt2sn  7253  suppssov1  7312  suppssfv  7316  brtpos  7346  wfrlem10  7409  wfrlem14  7413  wfrlem15  7414  seqomlem1  7530  seqomlem2  7531  omordi  7631  omord  7633  omwordi  7636  oeeui  7667  nnmordi  7696  nnmord  7697  nnmwordi  7700  nnawordex  7702  nnaordex  7703  nneob  7717  omsmolem  7718  qsss  7793  eroveu  7827  mapsncnv  7889  ralxpmap  7892  elixpsn  7932  ixpsnf1o  7933  boxcutc  7936  pw2f1olem  8049  2pwne  8101  mapxpen  8111  mapunen  8114  php  8129  unxpdomlem2  8150  en1eqsnbi  8176  isfiniteg  8205  fofinf1o  8226  f1opwfi  8255  elfiun  8321  oieu  8429  brwdom2  8463  wdomtr  8465  ixpiunwdom  8481  en3lplem1  8496  suc11reg  8501  inf3lemd  8509  cantnfvalf  8547  cantnflt  8554  cantnfp1lem3  8562  cantnflem2  8572  r1tr  8624  dfac8alem  8837  wdomnumr  8872  isinfcard  8900  aceq3lem  8928  dfac5lem4  8934  dfac5  8936  dfac2  8938  coftr  9080  fin23lem28  9147  fin23lem29  9148  fin1a2lem11  9217  fin1a2lem12  9218  fin1a2lem13  9219  hsmexlem9  9232  axdclem  9326  pwcfsdom  9390  gchdomtri  9436  fpwwe2  9450  gchpwdom  9477  gchhar  9486  addnidpi  9708  nqereu  9736  genpv  9806  genpdm  9809  distrlem5pr  9834  mulid1  10022  ltne  10119  mul02  10199  cnegex  10202  mul0or  10652  negfi  10956  sup2  10964  supaddc  10975  supadd  10976  supmul1  10977  supmul  10980  creur  10999  creui  11000  cju  11001  nnsub  11044  un0addcl  11311  un0mulcl  11312  nn0sub  11328  elz2  11379  zaddcl  11402  suprzcl2  11763  qmulz  11776  qre  11778  qnegcl  11790  xrmax1  11991  xrmin2  11994  max1ALT  12002  xlesubadd  12078  xmulass  12102  xlemul1a  12103  xrsupexmnf  12120  xrinfmexpnf  12121  xrub  12127  iccid  12205  fzsn  12368  fzsuc2  12383  fz1sbc  12400  elfzp12  12403  modmuladd  12695  seqid3  12828  bcval5  13088  bcpasc  13091  hashbnd  13106  hashnnn0genn0  13114  hashprg  13165  hashprgOLD  13166  hashfzo  13199  wrdl1s1  13377  cats1un  13457  shftlem  13789  replim  13837  absmod0  14024  absz  14032  rlimdm  14263  summolem2  14428  summo  14429  zsum  14430  fsum  14432  fsummulc2  14497  fsumconst  14503  fsum00  14511  incexclem  14549  isumsplit  14553  infcvgaux1i  14570  prodmolem2  14646  prodmo  14647  zprod  14648  fprod  14652  prodsn  14673  prodsnf  14675  fprodconst  14689  ruclem2  14942  fzo0dvdseq  15026  bitsf1ocnv  15147  sadcaddlem  15160  smueqlem  15193  gcdabs1  15232  bezoutlem1  15237  bezoutlem3  15239  bezoutlem4  15240  dvdsgcd  15242  dvdsmulgcd  15255  lcmgcdeq  15306  lcmf  15327  lcmfunsnlem1  15331  lcmfunsnlem2lem2  15333  dvdsprime  15381  isprm5  15400  coprm  15404  prmdvdsexpr  15410  rpexp  15413  phibndlem  15456  dfphi2  15460  hashgcdlem  15474  odzdvds  15481  nnoddn2prm  15497  pythagtriplem1  15502  iserodd  15521  pceulem  15531  pcqmul  15539  pcqcl  15542  pcxcl  15546  pcneg  15559  pcabs  15560  pcgcd1  15562  pcz  15566  pcprmpw2  15567  pcprmpw  15568  dvdsprmpweqle  15571  difsqpwdvds  15572  pcaddlem  15573  pcadd  15574  pcmpt  15577  pockthg  15591  prmreclem5  15605  4sqlem4  15637  mul4sq  15639  vdwapun  15659  vdwlem2  15667  vdwlem6  15671  vdwlem8  15673  vdwlem13  15678  0ram  15705  ram0  15707  ramcl  15714  cshwsiun  15787  wunress  15921  firest  16074  xpscfv  16203  isssc  16461  pospo  16954  latnlej  17049  gsumval2a  17260  mnd1id  17313  mulgnn0p1  17533  mulgnn0ass  17559  gicsubgen  17702  symg1bas  17797  psgnunilem1  17894  psgnunilem2  17896  mndodcongi  17943  oddvdsnn0  17944  odnncl  17945  oddvds  17947  odeq  17950  odeq1  17958  pgpfi2  18002  sylow2a  18015  sylow2blem3  18018  sylow3lem6  18028  lsmelvalm  18047  lsmsubm  18049  lsmsubg  18050  lsmmod  18069  lsmdisj2  18076  efgmnvl  18108  efgtlen  18120  efgs1b  18130  efgrelexlemb  18144  efgredeu  18146  efgcpbllemb  18149  frgpuptinv  18165  frgpup3lem  18171  qusabl  18249  frgpnabllem1  18257  cyggeninv  18266  cyggenod  18267  cygabl  18273  gsumval3eu  18286  dprdssv  18396  dprdfeq0  18402  dprdsubg  18404  dprddisj2  18419  ablfacrp  18446  pgpfac1lem3  18457  pgpfaclem2  18462  dvreq1  18674  irredn1  18687  drngmul0or  18749  isabvd  18801  abvdom  18819  issrngd  18842  lmodfopnelem2  18881  lss1d  18944  lspsneq0  18993  lbspss  19063  lsmcl  19064  lvecvs0or  19089  lspindpi  19113  lidl1el  19199  lpiss  19231  lidldvgen  19236  nzrunit  19248  rrgeq0  19271  domneq0  19278  mplsubrglem  19420  mplmonmul  19445  mplcoe5lem  19448  coe1tmmul2  19627  coe1tmmul  19628  pf1ind  19700  qsssubdrg  19786  zringlpirlem1  19813  znfld  19890  znunit  19893  znrrg  19895  cygznlem3  19899  frgpcyg  19903  psgnghm  19907  ipeq0  19964  cssincl  20013  lsmcss  20017  obselocv  20053  dsmmacl  20066  dsmmlss  20069  mat1dimelbas  20258  mdetralt  20395  mdetunilem2  20400  mdetunilem7  20405  mdetunilem9  20407  maducoeval2  20427  chpscmat  20628  chfacfscmulgsum  20646  chfacfpmmulgsum  20650  istopon  20698  eltg3  20747  tgidm  20765  clsval2  20835  opncldf1  20869  restbas  20943  tgrest  20944  restcld  20957  restcldr  20959  restcls  20966  restntr  20967  ordtbas2  20976  ordtbas  20977  ordtrest2lem  20988  ordtrest2  20989  pnfnei  21005  mnfnei  21006  tgcn  21037  cnconst  21069  cnindis  21077  lmss  21083  ordtt1  21164  discmp  21182  1stcrest  21237  2ndcdisj  21240  cldllycmp  21279  txbas  21351  ptpjpre1  21355  ptuni2  21360  ptbasin  21361  ptbasfi  21365  ptopn2  21368  txbasval  21390  ptpjopn  21396  ptclsg  21399  dfac14lem  21401  xkoccn  21403  ptcnp  21406  upxp  21407  ptrescn  21423  txkgen  21436  xkoptsub  21438  xkopt  21439  xkoco1cn  21441  xkoco2cn  21442  xkococn  21444  xkoinjcn  21471  ordthmeolem  21585  ptuncnv  21591  nrmhaus  21610  fbssint  21623  fbfinnfr  21626  fbasrn  21669  isufil2  21693  filufint  21705  rnelfm  21738  fmfnfmlem2  21740  fmfnfmlem3  21741  fmfnfmlem4  21742  fmfnfm  21743  flimtopon  21755  flimclslem  21769  fclstopon  21797  fclscf  21810  flimfnfcls  21813  alexsublem  21829  alexsubALTlem3  21834  alexsubALTlem4  21835  ptcmplem2  21838  tmdgsum2  21881  symgtgp  21886  cldsubg  21895  qustgplem  21905  tgptsmscld  21935  tsmsxplem1  21937  imasdsf1olem  22159  blssps  22210  blss  22211  stdbdxmet  22301  methaus  22306  metrest  22310  nrginvrcn  22477  nmoeq0  22521  blssioo  22579  xrtgioo  22590  xrsxmet  22593  reconnlem1  22610  reconnlem2  22611  xrge0tsms  22618  elcncf1di  22679  iccpnfcnv  22724  evth  22739  lebnumlem1  22741  lebnumlem2  22742  lebnumlem3  22743  nmoleub3  22900  minveclem3b  23180  ivthlem2  23202  ivthlem3  23203  elovolm  23224  ovolmge0  23226  ovoliun  23254  ovolicc2lem3  23268  ovolicc2  23271  voliunlem3  23301  dyaddisj  23345  dyadmax  23347  opnmblALT  23352  ismbfd  23388  ismbf2d  23389  mbfimaopnlem  23403  mbfimaopn2  23405  i1fmullem  23442  i1fres  23453  itg1climres  23462  mbfi1fseqlem4  23466  itg2lcl  23475  itgsplitioo  23585  ellimc2  23622  rolle  23734  dvlip  23737  dvge0  23750  dvne0  23755  lhop1lem  23757  tdeglem4  23801  degltlem1  23813  deg1nn0clb  23831  deg1lt0  23832  dvdsq1p  23901  ply1rem  23904  fta1g  23908  elply2  23933  plyf  23935  ne0p  23944  plyeq0lem  23947  plypf1  23949  0dgrb  23983  coe1termlem  23995  dgrcolem2  24011  plymul0or  24017  plyrem  24041  fta1  24044  quotcan  24045  aalioulem3  24070  eff1olem  24275  lognegb  24317  eflogeq  24329  argregt0  24337  argrege0  24338  tanarg  24346  cxpexp  24395  cxpeq0  24405  mulcxp  24412  cxpeq  24479  atans2  24639  scvxcvx  24693  dmgmaddn0  24730  isppw2  24822  vmappw  24823  vmacl  24825  efvmacl  24827  isnsqf  24842  mumullem2  24887  sqff1o  24889  dvdsppwf1o  24893  ppiublem1  24908  vmalelog  24911  chtublem  24917  fsumvma  24919  perfectlem2  24936  perfect  24937  bposlem1  24990  lgsmod  25029  lgsne0  25041  lgsdirnn0  25050  lgsqr  25057  lgsdchr  25061  gausslemma2dlem1a  25071  gausslemma2dlem6  25078  lgseisenlem2  25082  lgsquadlem1  25086  lgsquadlem2  25087  2lgslem1b  25098  2sqlem2  25124  mul2sq  25125  2sqlem7  25130  dchrisum0fno1  25181  pntrsumbnd2  25237  ostthlem1  25297  ostth2lem2  25304  ostth3  25308  ostth  25309  colinearalg  25771  axpasch  25802  axlowdimlem16  25818  axlowdimlem17  25819  axlowdim  25822  axcontlem2  25826  axcontlem4  25828  axcontlem7  25831  lpvtx  25944  edglnl  26019  numedglnl  26020  usgredgop  26046  usgrexmplef  26132  uhgrspansubgrlem  26163  uhgrspan1  26176  nbusgredgeu0  26251  nb3grprlem2  26264  cusgrsize2inds  26330  vtxd0nedgb  26365  rusgrpropnb  26460  upgrwlkvtxedg  26522  wlkp1lem1  26551  wlkp1lem6  26556  wlkp1lem8  26558  usgr2wlkneq  26633  crctcshwlk  26695  crctcsh  26697  wlkiswwlks1  26734  wlkwwlksur  26764  wwlksnextbi  26770  wwlksnextproplem2  26786  wspthsnonn0vne  26794  clwlkclwwlklem2  26882  clwwlksext2edg  26903  clwwisshclwws  26908  erclwwlkstr  26916  erclwwlksntr  26928  clwlksfclwwlk1hash  26940  0wlkons1  26962  3wlkdlem6  27005  eupth2eucrct  27057  frgrwopreglem2  27155  nvmul0or  27475  ipasslem5  27660  ipasslem11  27665  hvmul0or  27852  his6  27926  hhssnv  28091  ocsh  28112  ocin  28125  shsidmi  28213  chnlen0  28273  h1de2bi  28383  h1de2ctlem  28384  h1de2ci  28385  spansni  28386  3oalem1  28491  nmcexi  28855  atcveq0  29177  chcv1  29184  cdjreui  29261  cdj3lem2b  29266  xrge0tsmsd  29759  ordtrest2NEWlem  29942  ordtrest2NEW  29943  xrge0iifcnv  29953  esumc  30087  esumpcvgval  30114  ballotlemfc0  30528  ballotlemfcc  30529  bnj145OLD  30769  subfacp1lem4  31139  subfacp1lem5  31140  erdszelem8  31154  sconnpi1  31195  cvmsss2  31230  cvmlift2lem12  31270  msubco  31402  msubvrs  31431  sinccvglem  31540  untsucf  31561  dfpo2  31620  eqfunresadj  31635  dfrdg2  31675  trpred0  31710  frrlem4  31757  nolesgn2ores  31799  nolt02o  31819  nosupbnd2  31836  noetalem3  31839  colineardim1  32143  btwnconn1lem14  32182  segleantisym  32197  colinbtwnle  32200  outsidele  32214  lineunray  32229  linethru  32235  elicc3  32286  opnregcld  32300  cldregopn  32301  fnejoin2  32339  dissneqlem  33158  icorempt2  33170  relowlssretop  33182  relowlpssretop  33183  finxpsuclem  33205  lindsenlbs  33375  ptrecube  33380  poimirlem6  33386  poimirlem7  33387  poimirlem16  33396  poimirlem17  33397  poimirlem19  33399  poimirlem20  33400  poimirlem21  33401  poimirlem22  33402  poimirlem23  33403  poimirlem24  33404  poimirlem25  33405  poimirlem26  33406  poimirlem27  33407  poimirlem29  33409  poimirlem30  33410  poimirlem31  33411  poimirlem32  33412  itg2addnclem3  33434  ftc1anclem6  33461  dvasin  33467  unirep  33478  sdclem2  33509  ssbnd  33558  prdsbnd  33563  cntotbnd  33566  heibor1lem  33579  rrnequiv  33605  ismndo2  33644  grpoeqdivid  33651  isdrngo3  33729  crngohomfo  33776  0idl  33795  1idl  33796  divrngidl  33798  smprngopr  33822  prnc  33837  ispridlc  33840  riotaclbgBAD  34059  lshpdisj  34093  lsateln0  34101  lsatcveq0  34138  opnlen0  34294  cmtbr4N  34361  cvrnbtwn2  34381  cvrnbtwn4  34385  atcvreq0  34420  cvlatexch1  34442  exatleN  34509  atlelt  34543  ps-2  34583  llnn0  34621  lplnn0N  34652  islpln2a  34653  lvoln0N  34696  islvol2aN  34697  4at  34718  dalemcea  34765  dalem3  34769  pmapglb2N  34876  pmapglb2xN  34877  cdlema1N  34896  cdlemb  34899  paddasslem17  34941  llnexchb2lem  34973  llnexchb2  34974  lhpat3  35151  ltrnid  35240  trlne  35291  cdlemc4  35300  cdleme11h  35372  cdlemednuN  35406  cdlemg1a  35677  tendoeq2  35881  tendoid0  35932  dva1dim  36092  dib1dim  36273  dihlatat  36445  dochkrshp4  36497  dochkr1  36586  lclkrlem2e  36619  lcfrlem16  36666  lcfrlem28  36678  mapd0  36773  hdmap14lem13  36991  elrfi  37076  mrefg2  37089  eldiophb  37139  eldioph2b  37145  diophin  37155  diophun  37156  rexzrexnn0  37187  eldioph4b  37194  diophren  37196  rencldnfilem  37203  pellexlem6  37217  jm2.19  37379  rmydioph  37400  expdiophlem1  37407  expdioph  37409  lnr2i  37505  lpirlnr  37506  hbtlem2  37513  hbtlem4  37515  hbtlem6  37518  dgrsub2  37524  dgraa0p  37538  rngunsnply  37562  radcnvrat  38333  pm14.24  38453  addrcom  38499  afveu  40996  dfafn5b  41004  rlimdmafv  41020  el1fzopredsuc  41098  fmtnofac2lem  41245  proththdlem  41295  perfectALTVlem2  41396  perfectALTV  41397  gbowpos  41412  gbowgt5  41415  gboge9  41417  nnsum4primesodd  41449  nnsum4primesoddALTV  41450  sprvalpw  41495  lincellss  41980  lindsrng01  42022  suppdm  42065  nnpw2pb  42146
  Copyright terms: Public domain W3C validator