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  4243  preq1b  4409  elpreqprb  4428  reusv2lem2OLD  4900  reusv3  4906  alxfr  4908  reuhypd  4925  opth1  4973  euotd  5004  otiunsndisj  5009  tz7.2  5127  frsn  5223  elsnxp  5715  ordtri1  5794  ordtri3  5797  fvmptdv2  6337  fveqressseq  6395  foco2  6419  foco2OLD  6420  fsn  6442  fnsnb  6473  fmptsng  6475  fmptsnd  6476  fconst2g  6509  fnprb  6513  fntpb  6514  funfvima  6532  soisoi  6618  isores3  6625  riotaeqimp  6674  eusvobj2  6683  ovmpt2dv2  6836  f1opw2  6930  sorpssun  6986  sorpssin  6987  oneqmin  7047  nlimsucg  7084  onzsl  7088  tfinds  7101  funcnvuni  7161  opiota  7273  mpt2sn  7313  suppssov1  7372  suppssfv  7376  brtpos  7406  wfrlem10  7469  wfrlem14  7473  wfrlem15  7474  seqomlem1  7590  seqomlem2  7591  omordi  7691  omord  7693  omwordi  7696  oeeui  7727  nnmordi  7756  nnmord  7757  nnmwordi  7760  nnawordex  7762  nnaordex  7763  nneob  7777  omsmolem  7778  qsss  7851  eroveu  7885  mapsncnv  7946  ralxpmap  7949  elixpsn  7989  ixpsnf1o  7990  boxcutc  7993  pw2f1olem  8105  2pwne  8157  mapxpen  8167  mapunen  8170  php  8185  unxpdomlem2  8206  en1eqsnbi  8232  isfiniteg  8261  fofinf1o  8282  f1opwfi  8311  elfiun  8377  oieu  8485  brwdom2  8519  wdomtr  8521  ixpiunwdom  8537  en3lplem1  8549  suc11reg  8554  inf3lemd  8562  cantnfvalf  8600  cantnflt  8607  cantnfp1lem3  8615  cantnflem2  8625  r1tr  8677  dfac8alem  8890  wdomnumr  8925  isinfcard  8953  aceq3lem  8981  dfac5lem4  8987  dfac5  8989  dfac2  8991  coftr  9133  fin23lem28  9200  fin23lem29  9201  fin1a2lem11  9270  fin1a2lem12  9271  fin1a2lem13  9272  hsmexlem9  9285  axdclem  9379  pwcfsdom  9443  gchdomtri  9489  fpwwe2  9503  gchpwdom  9530  gchhar  9539  addnidpi  9761  nqereu  9789  genpv  9859  genpdm  9862  distrlem5pr  9887  mulid1  10075  ltne  10172  mul02  10252  cnegex  10255  mul0or  10705  negfi  11009  sup2  11017  supaddc  11028  supadd  11029  supmul1  11030  supmul  11033  creur  11052  creui  11053  cju  11054  nnsub  11097  un0addcl  11364  un0mulcl  11365  nn0sub  11381  elz2  11432  zaddcl  11455  suprzcl2  11816  qmulz  11829  qre  11831  qnegcl  11843  xrmax1  12044  xrmin2  12047  max1ALT  12055  xlesubadd  12131  xmulass  12155  xlemul1a  12156  xrsupexmnf  12173  xrinfmexpnf  12174  xrub  12180  iccid  12258  fzsn  12421  fzsuc2  12436  fz1sbc  12454  elfzp12  12457  modmuladd  12752  seqid3  12885  bcval5  13145  bcpasc  13148  hashbnd  13163  hashnnn0genn0  13171  hashprg  13220  hashprgOLD  13221  hashfzo  13254  wrdl1s1  13431  ccats1alpha  13436  cats1un  13521  shftlem  13852  replim  13900  absmod0  14087  absz  14095  rlimdm  14326  summolem2  14491  summo  14492  zsum  14493  fsum  14495  fsummulc2  14560  fsumconst  14566  fsum00  14574  incexclem  14612  isumsplit  14616  infcvgaux1i  14633  prodmolem2  14709  prodmo  14710  zprod  14711  fprod  14715  prodsn  14736  prodsnf  14738  fprodconst  14752  ruclem2  15005  fzo0dvdseq  15092  bitsf1ocnv  15213  sadcaddlem  15226  smueqlem  15259  gcdabs1  15298  bezoutlem1  15303  bezoutlem3  15305  bezoutlem4  15306  dvdsgcd  15308  dvdsmulgcd  15321  lcmgcdeq  15372  lcmf  15393  lcmfunsnlem1  15397  lcmfunsnlem2lem2  15399  isprm2lem  15441  dvdsprime  15447  isprm5  15466  coprm  15470  prmdvdsexpr  15476  rpexp  15479  phibndlem  15522  dfphi2  15526  hashgcdlem  15540  odzdvds  15547  nnoddn2prm  15563  pythagtriplem1  15568  iserodd  15587  pceulem  15597  pcqmul  15605  pcqcl  15608  pcxcl  15612  pcneg  15625  pcabs  15626  pcgcd1  15628  pcz  15632  pcprmpw2  15633  pcprmpw  15634  dvdsprmpweqle  15637  difsqpwdvds  15638  pcaddlem  15639  pcadd  15640  pcmpt  15643  pockthg  15657  prmreclem5  15671  4sqlem4  15703  mul4sq  15705  vdwapun  15725  vdwlem2  15733  vdwlem6  15737  vdwlem8  15739  vdwlem13  15744  0ram  15771  ram0  15773  ramcl  15780  cshwsiun  15853  wunress  15987  firest  16140  xpscfv  16269  isssc  16527  pospo  17020  latnlej  17115  gsumval2a  17326  mnd1id  17379  mulgnn0p1  17599  mulgnn0ass  17625  gicsubgen  17767  symg1bas  17862  psgnunilem1  17959  psgnunilem2  17961  mndodcongi  18008  oddvdsnn0  18009  odnncl  18010  oddvds  18012  odeq  18015  odeq1  18023  pgpfi2  18067  sylow2a  18080  sylow2blem3  18083  sylow3lem6  18093  lsmelvalm  18112  lsmsubm  18114  lsmsubg  18115  lsmmod  18134  lsmdisj2  18141  efgmnvl  18173  efgtlen  18185  efgs1b  18195  efgrelexlemb  18209  efgredeu  18211  efgcpbllemb  18214  frgpuptinv  18230  frgpup3lem  18236  qusabl  18314  frgpnabllem1  18322  cyggeninv  18331  cyggenod  18332  cygabl  18338  gsumval3eu  18351  dprdssv  18461  dprdfeq0  18467  dprdsubg  18469  dprddisj2  18484  ablfacrp  18511  pgpfac1lem3  18522  pgpfaclem2  18527  dvreq1  18739  irredn1  18752  drngmul0or  18816  isabvd  18868  abvdom  18886  issrngd  18909  lmodfopnelem2  18948  lss1d  19011  lspsneq0  19060  lbspss  19130  lsmcl  19131  lvecvs0or  19156  lspindpi  19180  lidl1el  19266  lpiss  19298  lidldvgen  19303  nzrunit  19315  rrgeq0  19338  domneq0  19345  mplsubrglem  19487  mplmonmul  19512  mplcoe5lem  19515  coe1tmmul2  19694  coe1tmmul  19695  pf1ind  19767  qsssubdrg  19853  zringlpirlem1  19880  znfld  19957  znunit  19960  znrrg  19962  cygznlem3  19966  frgpcyg  19970  psgnghm  19974  ipeq0  20031  cssincl  20080  lsmcss  20084  obselocv  20120  dsmmacl  20133  dsmmlss  20136  mat1dimelbas  20325  mdetralt  20462  mdetunilem2  20467  mdetunilem7  20472  mdetunilem9  20474  maducoeval2  20494  chpscmat  20695  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  istopon  20765  eltg3  20814  tgidm  20832  clsval2  20902  opncldf1  20936  restbas  21010  tgrest  21011  restcld  21024  restcldr  21026  restcls  21033  restntr  21034  ordtbas2  21043  ordtbas  21044  ordtrest2lem  21055  ordtrest2  21056  pnfnei  21072  mnfnei  21073  tgcn  21104  cnconst  21136  cnindis  21144  lmss  21150  ordtt1  21231  discmp  21249  1stcrest  21304  2ndcdisj  21307  cldllycmp  21346  txbas  21418  ptpjpre1  21422  ptuni2  21427  ptbasin  21428  ptbasfi  21432  ptopn2  21435  txbasval  21457  ptpjopn  21463  ptclsg  21466  dfac14lem  21468  xkoccn  21470  ptcnp  21473  upxp  21474  ptrescn  21490  txkgen  21503  xkoptsub  21505  xkopt  21506  xkoco1cn  21508  xkoco2cn  21509  xkococn  21511  xkoinjcn  21538  ordthmeolem  21652  ptuncnv  21658  nrmhaus  21677  fbssint  21689  fbfinnfr  21692  fbasrn  21735  isufil2  21759  filufint  21771  rnelfm  21804  fmfnfmlem2  21806  fmfnfmlem3  21807  fmfnfmlem4  21808  fmfnfm  21809  flimtopon  21821  flimclslem  21835  fclstopon  21863  fclscf  21876  flimfnfcls  21879  alexsublem  21895  alexsubALTlem3  21900  alexsubALTlem4  21901  ptcmplem2  21904  tmdgsum2  21947  symgtgp  21952  cldsubg  21961  qustgplem  21971  tgptsmscld  22001  tsmsxplem1  22003  imasdsf1olem  22225  blssps  22276  blss  22277  stdbdxmet  22367  methaus  22372  metrest  22376  nrginvrcn  22543  nmoeq0  22587  blssioo  22645  xrtgioo  22656  xrsxmet  22659  reconnlem1  22676  reconnlem2  22677  xrge0tsms  22684  elcncf1di  22745  iccpnfcnv  22790  evth  22805  lebnumlem1  22807  lebnumlem2  22808  lebnumlem3  22809  nmoleub3  22965  minveclem3b  23245  ivthlem2  23267  ivthlem3  23268  elovolm  23289  ovolmge0  23291  ovoliun  23319  ovolicc2lem3  23333  ovolicc2  23336  voliunlem3  23366  dyaddisj  23410  dyadmax  23412  opnmblALT  23417  ismbfd  23452  ismbf2d  23453  mbfimaopnlem  23467  mbfimaopn2  23469  i1fmullem  23506  i1fres  23517  itg1climres  23526  mbfi1fseqlem4  23530  itg2lcl  23539  itgsplitioo  23649  ellimc2  23686  rolle  23798  dvlip  23801  dvge0  23814  dvne0  23819  lhop1lem  23821  tdeglem4  23865  degltlem1  23877  deg1nn0clb  23895  deg1lt0  23896  dvdsq1p  23965  ply1rem  23968  fta1g  23972  elply2  23997  plyf  23999  ne0p  24008  plyeq0lem  24011  plypf1  24013  0dgrb  24047  coe1termlem  24059  dgrcolem2  24075  plymul0or  24081  plyrem  24105  fta1  24108  quotcan  24109  aalioulem3  24134  eff1olem  24339  lognegb  24381  eflogeq  24393  argregt0  24401  argrege0  24402  tanarg  24410  cxpexp  24459  cxpeq0  24469  mulcxp  24476  cxpeq  24543  atans2  24703  scvxcvx  24757  dmgmaddn0  24794  isppw2  24886  vmappw  24887  vmacl  24889  efvmacl  24891  isnsqf  24906  mumullem2  24951  sqff1o  24953  dvdsppwf1o  24957  ppiublem1  24972  vmalelog  24975  chtublem  24981  fsumvma  24983  perfectlem2  25000  perfect  25001  bposlem1  25054  lgsmod  25093  lgsne0  25105  lgsdirnn0  25114  lgsqr  25121  lgsdchr  25125  gausslemma2dlem1a  25135  gausslemma2dlem6  25142  lgseisenlem2  25146  lgsquadlem1  25150  lgsquadlem2  25151  2lgslem1b  25162  2sqlem2  25188  mul2sq  25189  2sqlem7  25194  dchrisum0fno1  25245  pntrsumbnd2  25301  ostthlem1  25361  ostth2lem2  25368  ostth3  25372  ostth  25373  colinearalg  25835  axpasch  25866  axlowdimlem16  25882  axlowdimlem17  25883  axlowdim  25886  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  lpvtx  26008  edglnl  26083  numedglnl  26084  usgredgop  26110  usgrexmplef  26196  uhgrspansubgrlem  26227  uhgrspan1  26240  nbusgredgeu0  26314  nb3grprlem2  26327  cusgrsize2inds  26405  vtxd0nedgb  26440  rusgrpropnb  26535  upgrwlkvtxedg  26597  wlkp1lem1  26626  wlkp1lem6  26631  wlkp1lem8  26633  usgr2wlkneq  26708  crctcshwlk  26770  crctcsh  26772  iswwlksnon  26802  wlkiswwlks1  26821  wlkwwlksur  26851  wwlksnextbi  26857  wwlksnextproplem2  26873  wspthsnonn0vne  26882  clwlkclwwlklem2  26966  clwwisshclwws  26972  erclwwlktr  26979  clwwlkext2edg  27020  erclwwlkntr  27035  clwlksfclwwlk1hash  27047  0wlkons1  27099  3wlkdlem6  27143  eupth2eucrct  27195  frgrwopreglem2  27293  clwwlknonccat  27334  2clwwlk2clwwlk  27338  nvmul0or  27633  ipasslem5  27818  ipasslem11  27823  hvmul0or  28010  his6  28084  hhssnv  28249  ocsh  28270  ocin  28283  shsidmi  28371  chnlen0  28431  h1de2bi  28541  h1de2ctlem  28542  h1de2ci  28543  spansni  28544  3oalem1  28649  nmcexi  29013  atcveq0  29335  chcv1  29342  cdjreui  29419  cdj3lem2b  29424  xrge0tsmsd  29913  ordtrest2NEWlem  30096  ordtrest2NEW  30097  xrge0iifcnv  30107  esumc  30241  esumpcvgval  30268  ballotlemfc0  30682  ballotlemfcc  30683  subfacp1lem4  31291  subfacp1lem5  31292  erdszelem8  31306  sconnpi1  31347  cvmsss2  31382  cvmlift2lem12  31422  msubco  31554  msubvrs  31583  sinccvglem  31692  untsucf  31713  dfpo2  31771  eqfunresadj  31785  dfrdg2  31825  trpred0  31860  nolesgn2ores  31950  nolt02o  31970  nosupbnd2  31987  noetalem3  31990  colineardim1  32293  btwnconn1lem14  32332  segleantisym  32347  colinbtwnle  32350  outsidele  32364  lineunray  32379  linethru  32385  elicc3  32436  opnregcld  32450  cldregopn  32451  fnejoin2  32489  dissneqlem  33317  icorempt2  33329  relowlssretop  33341  relowlpssretop  33342  finxpsuclem  33364  lindsenlbs  33534  ptrecube  33539  poimirlem6  33545  poimirlem7  33546  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  itg2addnclem3  33593  ftc1anclem6  33620  dvasin  33626  unirep  33637  sdclem2  33668  ssbnd  33717  prdsbnd  33722  cntotbnd  33725  heibor1lem  33738  rrnequiv  33764  ismndo2  33803  grpoeqdivid  33810  isdrngo3  33888  crngohomfo  33935  0idl  33954  1idl  33955  divrngidl  33957  smprngopr  33981  prnc  33996  ispridlc  33999  riotaclbgBAD  34558  lshpdisj  34592  lsateln0  34600  lsatcveq0  34637  opnlen0  34793  cmtbr4N  34860  cvrnbtwn2  34880  cvrnbtwn4  34884  atcvreq0  34919  cvlatexch1  34941  exatleN  35008  atlelt  35042  ps-2  35082  llnn0  35120  lplnn0N  35151  islpln2a  35152  lvoln0N  35195  islvol2aN  35196  4at  35217  dalemcea  35264  dalem3  35268  pmapglb2N  35375  pmapglb2xN  35376  cdlema1N  35395  cdlemb  35398  paddasslem17  35440  llnexchb2lem  35472  llnexchb2  35473  lhpat3  35650  ltrnid  35739  trlne  35790  cdlemc4  35799  cdleme11h  35871  cdlemednuN  35905  cdlemg1a  36175  tendoeq2  36379  tendoid0  36430  dva1dim  36590  dib1dim  36771  dihlatat  36943  dochkrshp4  36995  dochkr1  37084  lclkrlem2e  37117  lcfrlem16  37164  lcfrlem28  37176  mapd0  37271  hdmap14lem13  37489  elrfi  37574  mrefg2  37587  eldiophb  37637  eldioph2b  37643  diophin  37653  diophun  37654  rexzrexnn0  37685  eldioph4b  37692  diophren  37694  rencldnfilem  37701  pellexlem6  37715  jm2.19  37877  rmydioph  37898  expdiophlem1  37905  expdioph  37907  lnr2i  38003  lpirlnr  38004  hbtlem2  38011  hbtlem4  38013  hbtlem6  38016  dgrsub2  38022  dgraa0p  38036  rngunsnply  38060  radcnvrat  38830  pm14.24  38950  addrcom  38996  afveu  41554  dfafn5b  41562  rlimdmafv  41578  el1fzopredsuc  41660  fmtnofac2lem  41805  proththdlem  41855  perfectALTVlem2  41956  perfectALTV  41957  gbowpos  41972  gbowgt5  41975  gboge9  41977  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  sprvalpw  42055  lincellss  42540  lindsrng01  42582  suppdm  42625  nnpw2pb  42706
  Copyright terms: Public domain W3C validator