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

Theorem syl5ibrcom 225
Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)
Hypotheses
Ref Expression
syl5ibr.1  |-  ( ph  ->  th )
syl5ibr.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ibrcom  |-  ( ph  ->  ( ch  ->  ps ) )

Proof of Theorem syl5ibrcom
StepHypRef Expression
1 syl5ibr.1 . . 3  |-  ( ph  ->  th )
2 syl5ibr.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
31, 2syl5ibr 224 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
43com12 32 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  biimprcd  228  elsnc2g  4028  reusv2lem2  4626  reusv3  4632  alxfr  4634  reuhypd  4648  opth1  4694  euotd  4721  tz7.2  4837  ordtri1  5475  fvmptdv2  5979  fveqressseq  6033  foco2  6057  fsn  6076  fnsnb  6098  fmptsng  6100  fmptsnd  6101  fconst2g  6134  fnprb  6138  funfvima  6155  soisoi  6234  isores3  6241  eusvobj2  6298  ovmpt2dv2  6444  f1opw2  6536  sorpssun  6592  sorpssin  6593  oneqmin  6646  nlimsucg  6683  onzsl  6687  tfinds  6700  funcnvuni  6760  opiota  6866  mpt2sn  6898  suppssov1  6958  suppssfv  6962  brtpos  6993  wfrlem10  7056  wfrlem14  7060  wfrlem15  7061  seqomlem1  7178  seqomlem2  7179  omordi  7278  omord  7280  omwordi  7283  oeeui  7314  nnmordi  7343  nnmord  7344  nnmwordi  7347  nnawordex  7349  nnaordex  7350  nneob  7364  omsmolem  7365  qsss  7435  eroveu  7469  mapsncnv  7529  ralxpmap  7532  elixpsn  7572  ixpsnf1o  7573  boxcutc  7576  pw2f1olem  7685  2pwne  7737  mapxpen  7747  mapunen  7750  php  7765  unxpdomlem2  7786  en1eqsnbi  7811  isfiniteg  7840  fofinf1o  7861  f1opwfi  7887  elfiun  7953  oieu  8063  brwdom2  8097  wdomtr  8099  ixpiunwdom  8115  en3lplem1  8128  suc11reg  8133  inf3lemd  8141  cantnfvalf  8178  cantnflt  8185  cantnfp1lem3  8193  cantnflem2  8203  r1tr  8255  dfac8alem  8467  wdomnumr  8502  isinfcard  8530  aceq3lem  8558  dfac5lem4  8564  dfac5  8566  dfac2  8568  coftr  8710  fin23lem28  8777  fin23lem29  8778  fin1a2lem11  8847  fin1a2lem12  8848  fin1a2lem13  8849  hsmexlem9  8862  axdclem  8956  pwcfsdom  9015  gchdomtri  9061  fpwwe2  9075  gchpwdom  9102  gchhar  9111  addnidpi  9333  nqereu  9361  genpv  9431  genpdm  9434  distrlem5pr  9459  mulid1  9647  ltne  9737  mul02  9818  cnegex  9821  mul0or  10259  negfi  10561  sup2  10572  supaddc  10581  supadd  10582  supmul1  10583  supmul  10586  creur  10610  creui  10611  cju  10612  nnsub  10655  un0addcl  10910  un0mulcl  10911  nn0sub  10927  elz2  10961  zaddcl  10984  suprzcl2  11261  qmulz  11274  qre  11276  qnegcl  11288  xrmax1  11477  xrmin2  11480  max1ALT  11488  xlesubadd  11556  xmulass  11580  xlemul1a  11581  xrsupexmnf  11597  xrinfmexpnf  11598  xrub  11604  iccid  11688  fzsn  11847  fzsuc2  11860  fz1sbc  11877  elfzp12  11880  seqid3  12263  bcval5  12509  bcpasc  12512  hashbnd  12527  hashnnn0genn0  12532  hashprg  12578  hashfzo  12605  wrdl1s1  12753  cats1un  12834  shftlem  13131  replim  13179  absmod0  13366  absz  13374  rlimdm  13614  summolem2  13781  summo  13782  zsum  13783  fsum  13785  fsummulc2  13844  fsumconst  13850  fsum00  13857  incexclem  13893  isumsplit  13897  infcvgaux1i  13914  prodmolem2  13988  prodmo  13989  zprod  13990  fprod  13994  prodsn  14015  prodsnf  14017  fprodconst  14031  ruclem2  14283  fzo0dvdseq  14357  bitsf1ocnv  14417  sadcaddlem  14430  smueqlem  14463  gcdabs1  14497  bezoutlem1  14502  bezoutlem3OLD  14504  bezoutlem4OLD  14505  bezoutlem3  14507  bezoutlem4  14508  dvdsgcd  14510  dvdsmulgcd  14521  lcmgcdeq  14576  lcmf  14605  lcmfunsnlem1  14609  lcmfunsnlem2lem2  14611  dvdsprime  14636  isprm5  14650  coprm  14656  prmdvdsexpr  14668  rpexp  14671  phibndlem  14717  dfphi2  14721  odzdvds  14739  odzdvdsOLD  14745  pythagtriplem1  14765  iserodd  14784  pceulem  14794  pcqmul  14802  pcqcl  14805  pcxcl  14809  pcneg  14822  pcabs  14823  pcgcd1  14825  pcz  14829  pcprmpw2  14830  pcprmpw  14831  pcaddlem  14832  pcadd  14833  pcmpt  14836  pockthg  14849  prmreclem5  14863  4sqlem4  14895  mul4sq  14897  vdwapun  14923  vdwlem2  14931  vdwlem6  14935  vdwlem8  14937  vdwlem13  14942  0ram  14977  ram0  14979  ramcl  14986  cshwsiun  15069  wunress  15188  firest  15330  xpscfv  15467  isssc  15724  pospo  16218  latnlej  16313  gsumval2a  16521  mnd1id  16578  mulgnn0p1  16768  mulgnn0ass  16786  gicsubgen  16941  symg1bas  17036  psgnunilem1  17133  psgnunilem2  17135  mndodcongi  17191  oddvdsnn0  17192  odnncl  17193  oddvds  17195  odeq  17198  odeq1  17210  pgpfi2  17257  sylow2a  17270  sylow2blem3  17273  sylow3lem6  17283  lsmelvalm  17302  lsmsubm  17304  lsmsubg  17305  lsmmod  17324  lsmdisj2  17331  efgmnvl  17363  efgtlen  17375  efgs1b  17385  efgrelexlemb  17399  efgredeu  17401  efgcpbllemb  17404  frgpuptinv  17420  frgpup3lem  17426  qusabl  17502  frgpnabllem1  17508  cyggeninv  17517  cyggenod  17518  cygabl  17524  gsumval3eu  17537  dprdssv  17648  dprdfeq0  17654  dprdsubg  17656  dprddisj2  17671  ablfacrp  17698  pgpfac1lem3  17709  pgpfaclem2  17714  dvreq1  17920  irredn1  17933  drngmul0or  17995  isabvd  18047  abvdom  18065  issrngd  18088  lss1d  18185  lspsneq0  18234  lbspss  18304  lsmcl  18305  lvecvs0or  18330  lspindpi  18354  lidl1el  18441  lpiss  18473  lidldvgen  18478  nzrunit  18490  rrgeq0  18513  domneq0  18520  mplsubrglem  18662  mplmonmul  18687  mplcoe5lem  18690  coe1tmmul2  18868  coe1tmmul  18869  pf1ind  18942  qsssubdrg  19026  zringlpirlem1  19051  znfld  19129  znunit  19132  znrrg  19134  cygznlem3  19138  frgpcyg  19142  psgnghm  19146  ipeq0  19203  cssincl  19249  lsmcss  19253  obselocv  19289  dsmmacl  19302  dsmmlss  19305  mat1dimelbas  19494  mdetralt  19631  mdetunilem2  19636  mdetunilem7  19641  mdetunilem9  19643  maducoeval2  19663  chpscmat  19864  chfacfscmulgsum  19882  chfacfpmmulgsum  19886  istopon  19938  eltg3  19975  tgidm  19994  clsval2  20063  opncldf1  20098  restbas  20172  tgrest  20173  restcld  20186  restcldr  20188  restcls  20195  restntr  20196  ordtbas2  20205  ordtbas  20206  ordtrest2lem  20217  ordtrest2  20218  pnfnei  20234  mnfnei  20235  tgcn  20266  cnconst  20298  cnindis  20306  lmss  20312  ordtt1  20393  discmp  20411  1stcrest  20466  2ndcdisj  20469  cldllycmp  20508  txbas  20580  ptpjpre1  20584  ptuni2  20589  ptbasin  20590  ptbasfi  20594  ptopn2  20597  txbasval  20619  ptpjopn  20625  ptclsg  20628  dfac14lem  20630  xkoccn  20632  ptcnp  20635  upxp  20636  ptrescn  20652  txkgen  20665  xkoptsub  20667  xkopt  20668  xkoco1cn  20670  xkoco2cn  20671  xkococn  20673  xkoinjcn  20700  ordthmeolem  20814  ptuncnv  20820  nrmhaus  20839  fbssint  20851  fbfinnfr  20854  fbasrn  20897  isufil2  20921  filufint  20933  rnelfm  20966  fmfnfmlem2  20968  fmfnfmlem3  20969  fmfnfmlem4  20970  fmfnfm  20971  flimtopon  20983  flimclslem  20997  fclstopon  21025  fclscf  21038  flimfnfcls  21041  alexsublem  21057  alexsubALTlem3  21062  alexsubALTlem4  21063  ptcmplem2  21066  tmdgsum2  21109  symgtgp  21114  cldsubg  21123  qustgplem  21133  tgptsmscld  21163  tsmsxplem1  21165  imasdsf1olem  21386  blssps  21437  blss  21438  stdbdxmet  21528  methaus  21533  metrest  21537  nrginvrcn  21692  nmoeq0  21755  blssioo  21811  xrtgioo  21822  xrsxmet  21825  reconnlem1  21842  reconnlem2  21843  xrge0tsms  21850  elcncf1di  21925  iccpnfcnv  21970  evth  21985  lebnumlem1  21987  lebnumlem2  21988  lebnumlem3  21989  lebnumlem1OLD  21990  lebnumlem2OLD  21991  lebnumlem3OLD  21992  nmoleub3  22131  minveclem3b  22368  minveclem3bOLD  22380  ivthlem2  22401  ivthlem3  22402  elovolm  22426  ovolmge0  22428  ovoliun  22456  ovolicc2lem3  22470  ovolicc2  22474  voliunlem3  22503  dyaddisj  22552  dyadmax  22554  opnmblALT  22559  ismbfd  22594  ismbf2d  22595  mbfimaopnlem  22609  mbfimaopn2  22611  i1fmullem  22650  i1fres  22661  itg1climres  22670  mbfi1fseqlem4  22674  itg2lcl  22683  itgsplitioo  22793  ellimc2  22830  rolle  22940  dvlip  22943  dvge0  22956  dvne0  22961  lhop1lem  22963  tdeglem4  23007  degltlem1  23019  deg1nn0clb  23037  deg1lt0  23038  dvdsq1p  23109  ply1rem  23112  fta1g  23116  elply2  23148  plyf  23150  ne0p  23159  plyeq0lem  23162  plypf1  23164  0dgrb  23198  coe1termlem  23210  dgrcolem2  23226  plymul0or  23232  plyrem  23256  fta1  23259  quotcan  23260  aalioulem3  23288  eff1olem  23495  lognegb  23537  eflogeq  23549  argregt0  23557  argrege0  23558  tanarg  23566  cxpexp  23611  cxpeq0  23621  mulcxp  23628  cxpeq  23695  atans2  23855  scvxcvx  23909  dmgmaddn0  23946  isppw2  24040  vmappw  24041  vmacl  24043  efvmacl  24045  isnsqf  24060  mumullem2  24105  sqff1o  24107  dvdsppwf1o  24113  ppiublem1  24128  vmalelog  24131  chtublem  24137  fsumvma  24139  perfectlem2  24156  perfect  24157  bposlem1  24210  lgsmod  24247  lgsne0  24259  lgsdirnn0  24265  lgsqr  24272  lgsdchr  24274  lgseisenlem2  24276  lgsquadlem1  24280  lgsquadlem2  24281  2sqlem2  24290  mul2sq  24291  2sqlem7  24296  dchrisum0fno1  24347  pntrsumbnd2  24403  ostthlem1  24463  ostth2lem2  24470  ostth3  24474  ostth  24475  colinearalg  24938  axpasch  24969  axlowdimlem16  24985  axlowdimlem17  24986  axlowdim  24989  axcontlem2  24993  axcontlem4  24995  axcontlem7  24998  usgraexmplef  25126  nbgraf1olem1  25167  nbgraf1olem3  25169  nbgraf1olem5  25171  nb3graprlem2  25178  cusgrasize2inds  25203  wlklenvm1  25258  wlkiswwlksur  25445  wwlknextbi  25451  wwlkextproplem2  25468  clwlkisclwwlklem1  25513  clwwisshclww  25533  erclwwlktr  25541  erclwwlkntr  25553  clwlkfclwwlk1hash  25568  vdgr1a  25632  vdusgra0nedg  25634  usgravd0nedg  25644  0eusgraiff0rgra  25665  rusgraprop2  25668  eupap1  25702  vdn0frgrav2  25749  vdgn0frgrav2  25750  ismndo2  26071  ghgrplem1OLD  26092  nvmul0or  26271  ipasslem5  26474  ipasslem11  26479  hvmul0or  26676  his6  26750  hhssnv  26913  ocsh  26934  ocin  26947  shsidmi  27035  chnlen0  27095  h1de2bi  27205  h1de2ctlem  27206  h1de2ci  27207  spansni  27208  3oalem1  27313  nmcexi  27677  atcveq0  27999  chcv1  28006  cdjreui  28083  cdj3lem2b  28088  xrge0tsmsd  28556  ordtrest2NEWlem  28736  ordtrest2NEW  28737  xrge0iifcnv  28747  esumc  28880  esumpcvgval  28907  ballotlemfc0  29333  ballotlemfcc  29334  bnj145OLD  29543  subfacp1lem4  29914  subfacp1lem5  29915  erdszelem8  29929  sconpi1  29970  cvmsss2  30005  cvmlift2lem12  30045  msubco  30177  msubvrs  30206  sinccvglem  30324  untsucf  30345  dfpo2  30402  dfrdg2  30449  trpred0  30484  frrlem4  30524  colineardim1  30833  btwnconn1lem14  30872  segleantisym  30887  colinbtwnle  30890  outsidele  30904  lineunray  30919  linethru  30925  elicc3  30978  opnregcld  30991  cldregopn  30992  fnejoin2  31030  dissneqlem  31706  icorempt2  31718  relowlssretop  31730  relowlpssretop  31731  finxpsuclem  31753  ptrecube  31904  poimirlem6  31910  poimirlem7  31911  poimirlem16  31920  poimirlem17  31921  poimirlem19  31923  poimirlem20  31924  poimirlem21  31925  poimirlem22  31926  poimirlem23  31927  poimirlem24  31928  poimirlem25  31929  poimirlem26  31930  poimirlem27  31931  poimirlem29  31933  poimirlem30  31934  poimirlem31  31935  poimirlem32  31936  itg2addnclem3  31959  ftc1anclem6  31986  dvasin  31992  unirep  32003  sdclem2  32035  ssbnd  32084  prdsbnd  32089  cntotbnd  32092  heibor1lem  32105  rrnequiv  32131  grpoeqdivid  32143  isdrngo3  32162  crngohomfo  32203  0idl  32222  1idl  32223  divrngidl  32225  smprngopr  32249  prnc  32264  ispridlc  32267  riotaclbgBAD  32495  lshpdisj  32522  lsateln0  32530  lsatcveq0  32567  opnlen0  32723  cmtbr4N  32790  cvrnbtwn2  32810  cvrnbtwn4  32814  atcvreq0  32849  cvlatexch1  32871  exatleN  32938  atlelt  32972  ps-2  33012  llnn0  33050  lplnn0N  33081  islpln2a  33082  lvoln0N  33125  islvol2aN  33126  4at  33147  dalemcea  33194  dalem3  33198  pmapglb2N  33305  pmapglb2xN  33306  cdlema1N  33325  cdlemb  33328  paddasslem17  33370  llnexchb2lem  33402  llnexchb2  33403  lhpat3  33580  ltrnid  33669  trlne  33720  cdlemc4  33729  cdleme11h  33801  cdlemednuN  33835  cdlemg1a  34106  tendoeq2  34310  tendoid0  34361  dva1dim  34521  dib1dim  34702  dihlatat  34874  dochkrshp4  34926  dochkr1  35015  lclkrlem2e  35048  lcfrlem16  35095  lcfrlem28  35107  mapd0  35202  hdmap14lem13  35420  elrfi  35505  mrefg2  35518  eldiophb  35568  eldioph2b  35574  diophin  35584  diophun  35585  rexzrexnn0  35616  eldioph4b  35623  diophren  35625  rencldnfilem  35632  pellexlem6  35648  jm2.19  35818  rmydioph  35839  expdiophlem1  35846  expdioph  35848  lnr2i  35945  lpirlnr  35946  hbtlem2  35953  hbtlem4  35955  hbtlem6  35958  dgrsub2  35964  dgraa0p  35985  rngunsnply  36009  hashgcdlem  36044  radcnvrat  36633  pm14.24  36753  addrcom  36798  afveu  38525  dfafn5b  38533  rlimdmafv  38549  el1fzopredsuc  38592  perfectALTVlem2  38714  perfectALTV  38715  gbopos  38730  gbogt5  38733  gboage9  38735  nnsum4primesodd  38761  nnsum4primesoddALTV  38762  proththdlem  38783  uhgrauhgr  38990  usgredgop  39051  uhgrspansubgrlem  39133  uhgrspan1  39144  nbusgredgeu0  39206  nb3grprlem2  39214  cusgrsize2inds  39270  uhgrauhg  39304  lincellss  39840  lindsrng01  39882  suppdm  39925  nnpw2pb  40019
  Copyright terms: Public domain W3C validator