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

Theorem syl5ibrcom 222
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 221 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
43com12 31 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  biimprcd  225  elsnc2g  4040  reusv2lem2  4635  reusv3  4641  alxfr  4646  reuhypd  4660  opth1  4706  euotd  4734  tz7.2  4849  ordtri1  4897  xpsspw  5102  fvmptdv2  5950  fveqressseq  6008  foco2  6032  fsn  6050  fnsnb  6071  fmptsng  6073  fmptsnd  6074  fconst2g  6106  fnprb  6110  fnprOLD  6111  funfvima  6128  soisoi  6205  isores3  6212  eusvobj2  6270  ovmpt2dv2  6417  f1opw2  6509  suppssfvOLD  6512  suppssov1OLD  6513  sorpssun  6568  sorpssin  6569  oneqmin  6621  nlimsucg  6658  onzsl  6662  tfinds  6675  funcnvuni  6734  opiota  6840  mpt2sn  6872  suppssov1  6930  suppssfv  6934  brtpos  6962  seqomlem1  7113  seqomlem2  7114  omordi  7213  omord  7215  omwordi  7218  oeeui  7249  nnmordi  7278  nnmord  7279  nnmwordi  7282  nnawordex  7284  nnaordex  7285  nneob  7299  omsmolem  7300  qsss  7370  eroveu  7404  mapsncnv  7463  ralxpmap  7466  elixpsn  7506  ixpsnf1o  7507  boxcutc  7510  pw2f1olem  7619  2pwne  7671  mapxpen  7681  mapunen  7684  php  7699  unxpdomlem2  7723  en1eqsnbi  7748  isfiniteg  7778  fofinf1o  7799  f1opwfi  7822  elfiun  7888  oieu  7962  brwdom2  7997  wdomtr  7999  ixpiunwdom  8015  en3lplem1  8029  suc11reg  8034  inf3lemd  8042  cantnfvalf  8082  cantnflt  8089  cantnfp1lem3  8097  cantnflem2  8107  cantnfltOLD  8119  cantnfp1lem3OLD  8123  r1tr  8192  dfac8alem  8408  wdomnumr  8443  isinfcard  8471  aceq3lem  8499  dfac5lem4  8505  dfac5  8507  dfac2  8509  coftr  8651  fin23lem28  8718  fin23lem29  8719  fin1a2lem11  8788  fin1a2lem12  8789  fin1a2lem13  8790  hsmexlem9  8803  axdclem  8897  pwcfsdom  8956  gchdomtri  9005  fpwwe2  9019  gchpwdom  9046  gchhar  9055  addnidpi  9277  nqereu  9305  genpv  9375  genpdm  9378  distrlem5pr  9403  mulid1  9591  ltne  9679  mul02  9756  cnegex  9759  mul0or  10190  sup2  10500  supmul1  10509  supmul  10512  creur  10531  creui  10532  cju  10533  nnsub  10575  un0addcl  10830  un0mulcl  10831  nn0sub  10847  elz2  10882  zaddcl  10905  suprzcl2  11176  qmulz  11189  qre  11191  qnegcl  11203  xrmax1  11380  xrmin2  11383  max1ALT  11391  xlesubadd  11459  xmulass  11483  xlemul1a  11484  xrsupexmnf  11500  xrinfmexpnf  11501  xrub  11507  iccid  11578  fzsn  11729  fzsuc2  11741  fz1sbc  11758  elfzp12  11761  fzm1  11762  seqid3  12125  bcval5  12370  bcpasc  12373  hashbnd  12385  hashnnn0genn0  12390  hashprg  12434  hashfzo  12461  wrdl1s1  12596  cats1un  12675  shftlem  12875  replim  12923  absmod0  13110  absz  13118  rlimdm  13348  summolem2  13512  summo  13513  zsum  13514  fsum  13516  fsummulc2  13573  fsumconst  13579  fsum00  13586  incexclem  13622  isumsplit  13626  infcvgaux1i  13642  ruclem2  13837  fzo0dvdseq  13911  bitsf1ocnv  13966  sadcaddlem  13979  smueqlem  14012  gcdabs1  14044  bezoutlem1  14048  bezoutlem3  14050  bezoutlem4  14051  dvdsgcd  14053  dvdsmulgcd  14064  dvdsprime  14102  coprm  14113  isprm5  14125  prmdvdsexpr  14129  rpexp  14133  phibndlem  14172  dfphi2  14176  odzdvds  14194  pythagtriplem1  14212  iserodd  14231  pceulem  14241  pcqmul  14249  pcqcl  14252  pcxcl  14256  pcneg  14269  pcabs  14270  pcgcd1  14272  pcz  14276  pcprmpw2  14277  pcprmpw  14278  pcaddlem  14279  pcadd  14280  pcmpt  14283  pockthg  14296  prmreclem5  14310  4sqlem4  14342  mul4sq  14344  vdwapun  14364  vdwlem2  14372  vdwlem6  14376  vdwlem8  14378  vdwlem13  14383  0ram  14410  ram0  14412  ramcl  14419  cshwsiun  14456  wunress  14568  firest  14702  xpscfv  14831  isssc  15061  pospo  15472  latnlej  15567  gsumval2a  15775  mnd1id  15832  mulgnn0p1  16022  mulgnn0ass  16040  gicsubgen  16195  symg1bas  16290  psgnunilem1  16387  psgnunilem2  16389  mndodcongi  16436  oddvdsnn0  16437  odnncl  16438  oddvds  16440  odeq  16443  odeq1  16451  pgpfi2  16495  sylow2a  16508  sylow2blem3  16511  sylow3lem6  16521  lsmelvalm  16540  lsmsubm  16542  lsmsubg  16543  lsmmod  16562  lsmdisj2  16569  efgmnvl  16601  efgtlen  16613  efgs1b  16623  efgrelexlemb  16637  efgredeu  16639  efgcpbllemb  16642  frgpuptinv  16658  frgpup3lem  16664  qusabl  16740  frgpnabllem1  16746  cyggeninv  16755  cyggenod  16756  cygabl  16762  gsumval3eu  16776  dprdssv  16924  dprdfeq0  16930  dprdfeq0OLD  16937  dprdsubg  16939  dprddisj2  16955  dprddisj2OLD  16956  ablfacrp  16985  pgpfac1lem3  16996  pgpfaclem2  17001  dvreq1  17210  irredn1  17223  drngmul0or  17285  isabvd  17337  abvdom  17355  issrngd  17378  lss1d  17477  lspsneq0  17526  lbspss  17596  lsmcl  17597  lvecvs0or  17622  lspindpi  17646  lidl1el  17734  lpiss  17766  lidldvgen  17771  nzrunit  17783  rrgeq0  17806  domneq0  17814  mplsubrglem  17968  mplsubrglemOLD  17969  mplmonmul  17994  mplcoe5lem  17998  coe1tmmul2  18185  coe1tmmul  18186  pf1ind  18259  qsssubdrg  18345  zringlpirlem1  18376  zlpirlem1  18381  znfld  18466  znunit  18469  znrrg  18471  cygznlem3  18475  frgpcyg  18479  psgnghm  18483  ipeq0  18540  cssincl  18586  lsmcss  18590  obselocv  18626  dsmmacl  18639  dsmmlss  18642  mat1dimelbas  18840  mdetralt  18977  mdetunilem2  18982  mdetunilem7  18987  mdetunilem9  18989  maducoeval2  19009  chpscmat  19210  chfacfscmulgsum  19228  chfacfpmmulgsum  19232  istopon  19293  eltg3  19330  tgidm  19348  clsval2  19417  opncldf1  19451  restbas  19525  tgrest  19526  restcld  19539  restcldr  19541  restcls  19548  restntr  19549  ordtbas2  19558  ordtbas  19559  ordtrest2lem  19570  ordtrest2  19571  pnfnei  19587  mnfnei  19588  tgcn  19619  cnconst  19651  cnindis  19659  lmss  19665  ordtt1  19746  discmp  19764  1stcrest  19820  2ndcdisj  19823  cldllycmp  19862  txbas  19934  ptpjpre1  19938  ptuni2  19943  ptbasin  19944  ptbasfi  19948  ptopn2  19951  txbasval  19973  ptpjopn  19979  ptclsg  19982  dfac14lem  19984  xkoccn  19986  ptcnp  19989  upxp  19990  ptrescn  20006  txkgen  20019  xkoptsub  20021  xkopt  20022  xkoco1cn  20024  xkoco2cn  20025  xkococn  20027  xkoinjcn  20054  ordthmeolem  20168  ptuncnv  20174  nrmhaus  20193  fbssint  20205  fbfinnfr  20208  fbasrn  20251  isufil2  20275  filufint  20287  rnelfm  20320  fmfnfmlem2  20322  fmfnfmlem3  20323  fmfnfmlem4  20324  fmfnfm  20325  flimtopon  20337  flimclslem  20351  fclstopon  20379  fclscf  20392  flimfnfcls  20395  alexsublem  20410  alexsubALTlem3  20415  alexsubALTlem4  20416  ptcmplem2  20419  tmdgsum2  20461  symgtgp  20466  cldsubg  20475  qustgplem  20485  tgptsmscld  20519  tsmsxplem1  20521  imasdsf1olem  20742  blssps  20793  blss  20794  stdbdxmet  20884  methaus  20889  metrest  20893  nrginvrcn  21066  nmoeq0  21109  blssioo  21166  xrtgioo  21177  xrsxmet  21180  reconnlem1  21197  reconnlem2  21198  xrge0tsms  21205  elcncf1di  21265  iccpnfcnv  21310  evth  21325  lebnumlem1  21327  lebnumlem2  21328  lebnumlem3  21329  nmoleub3  21468  minveclem3b  21709  ivthlem2  21730  ivthlem3  21731  elovolm  21752  ovolmge0  21754  ovoliun  21782  ovolicc2lem3  21796  ovolicc2  21799  voliunlem3  21828  dyaddisj  21871  dyadmax  21873  opnmblALT  21878  ismbfd  21913  ismbf2d  21914  mbfimaopnlem  21928  mbfimaopn2  21930  i1fmullem  21967  i1fres  21978  itg1climres  21987  mbfi1fseqlem4  21991  itg2lcl  22000  itgsplitioo  22110  ellimc2  22147  rolle  22257  dvlip  22260  dvge0  22273  dvne0  22278  lhop1lem  22280  tdeglem4  22324  degltlem1  22338  deg1nn0clb  22356  deg1lt0  22357  dvdsq1p  22427  ply1rem  22430  fta1g  22434  elply2  22459  plyf  22461  ne0p  22470  plyeq0lem  22473  plypf1  22475  0dgrb  22509  coe1termlem  22520  dgrcolem2  22536  plymul0or  22542  plyrem  22566  fta1  22569  quotcan  22570  aalioulem3  22595  eff1olem  22800  lognegb  22839  eflogeq  22851  argregt0  22860  argrege0  22861  tanarg  22869  cxpexp  22914  cxpeq0  22924  mulcxp  22931  cxpeq  22996  atans2  23127  scvxcvx  23180  isppw2  23254  vmappw  23255  vmacl  23257  efvmacl  23259  isnsqf  23274  mumullem2  23319  sqff1o  23321  dvdsppwf1o  23327  ppiublem1  23342  vmalelog  23345  chtublem  23351  fsumvma  23353  perfectlem2  23370  perfect  23371  bposlem1  23424  lgsmod  23461  lgsne0  23473  lgsdirnn0  23479  lgsqr  23486  lgsdchr  23488  lgseisenlem2  23490  lgsquadlem1  23494  lgsquadlem2  23495  2sqlem2  23504  mul2sq  23505  2sqlem7  23510  dchrisum0fno1  23561  pntrsumbnd2  23617  ostthlem1  23677  ostth2lem2  23684  ostth3  23688  ostth  23689  colinearalg  24078  axpasch  24109  axlowdimlem16  24125  axlowdimlem17  24126  axlowdim  24129  axcontlem2  24133  axcontlem4  24135  axcontlem7  24138  usgraexmpl  24266  nbgraf1olem1  24306  nbgraf1olem3  24308  nbgraf1olem5  24310  nb3graprlem2  24317  cusgrasize2inds  24342  wlklenvm1  24397  wlkiswwlksur  24584  wwlknextbi  24590  wwlkextproplem2  24607  clwlkisclwwlklem1  24652  clwwisshclww  24672  erclwwlktr  24680  erclwwlkntr  24692  clwlkfclwwlk1hash  24707  vdgr1a  24771  vdusgra0nedg  24773  usgravd0nedg  24783  0eusgraiff0rgra  24804  rusgraprop2  24807  eupap1  24841  vdn0frgrav2  24888  vdgn0frgrav2  24889  ismndo2  25212  ghgrplem1OLD  25233  nvmul0or  25412  ipasslem5  25615  ipasslem11  25620  hvmul0or  25807  his6  25881  hhssnv  26045  ocsh  26066  ocin  26079  shsidmi  26167  chnlen0  26227  h1de2bi  26337  h1de2ctlem  26338  h1de2ci  26339  spansni  26340  3oalem1  26445  nmcexi  26810  atcveq0  27132  chcv1  27139  cdjreui  27216  cdj3lem2b  27221  xrge0tsmsd  27641  ordtrest2NEWlem  27770  ordtrest2NEW  27771  xrge0iifcnv  27781  esumc  27928  esumpcvgval  27950  ballotlemfc0  28297  ballotlemfcc  28298  dmgmaddn0  28431  subfacp1lem4  28493  subfacp1lem5  28494  erdszelem8  28508  sconpi1  28550  cvmsss2  28585  cvmlift2lem12  28625  msubco  28757  msubvrs  28786  sinccvglem  28904  untsucf  28948  prodmolem2  29035  prodmo  29036  zprod  29037  fprod  29041  prodsn  29060  fprodconst  29076  dfpo2  29152  dfrdg2  29196  trpred0  29287  wfrlem10  29320  wfrlem14  29324  wfrlem15  29325  frrlem4  29358  colineardim1  29679  btwnconn1lem14  29718  segleantisym  29733  colinbtwnle  29736  outsidele  29750  lineunray  29765  linethru  29771  supaddc  30009  supadd  30010  itg2addnclem3  30036  ftc1anclem6  30063  dvasin  30071  elicc3  30103  opnregcld  30116  cldregopn  30117  fnejoin2  30155  unirep  30171  sdclem2  30203  ssbnd  30252  prdsbnd  30257  cntotbnd  30260  heibor1lem  30273  rrnequiv  30299  grpoeqdivid  30311  isdrngo3  30330  crngohomfo  30371  0idl  30390  1idl  30391  divrngidl  30393  smprngopr  30417  prnc  30432  ispridlc  30435  elrfi  30594  mrefg2  30607  eldiophb  30658  eldioph2b  30664  diophin  30674  diophun  30675  rexzrexnn0  30705  eldioph4b  30713  diophren  30715  rencldnfilem  30722  pellexlem6  30738  jm2.19  30903  rmydioph  30924  expdiophlem1  30931  expdioph  30933  lnr2i  31033  lpirlnr  31034  hbtlem2  31041  hbtlem4  31043  hbtlem6  31046  dgrsub2  31052  dgraa0p  31067  rngunsnply  31091  hashgcdlem  31126  radcnvrat  31164  lcmgcdeq  31185  pm14.24  31286  addrcom  31331  afveu  32072  dfafn5b  32080  rlimdmafv  32096  uhgrauhg  32207  lincellss  32737  lindsrng01  32779  bnj145OLD  33490  riotaclbgBAD  34387  lshpdisj  34414  lsateln0  34422  lsatcveq0  34459  opnlen0  34615  cmtbr4N  34682  cvrnbtwn2  34702  cvrnbtwn4  34706  atcvreq0  34741  cvlatexch1  34763  exatleN  34830  atlelt  34864  ps-2  34904  llnn0  34942  lplnn0N  34973  islpln2a  34974  lvoln0N  35017  islvol2aN  35018  4at  35039  dalemcea  35086  dalem3  35090  pmapglb2N  35197  pmapglb2xN  35198  cdlema1N  35217  cdlemb  35220  paddasslem17  35262  llnexchb2lem  35294  llnexchb2  35295  lhpat3  35472  ltrnid  35561  trlne  35612  cdlemc4  35621  cdleme11h  35693  cdlemednuN  35727  cdlemg1a  35998  tendoeq2  36202  tendoid0  36253  dva1dim  36413  dib1dim  36594  dihlatat  36766  dochkrshp4  36818  dochkr1  36907  lclkrlem2e  36940  lcfrlem16  36987  lcfrlem28  36999  mapd0  37094  hdmap14lem13  37312
  Copyright terms: Public domain W3C validator