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

Theorem syl5ibrcom 230
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 229 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
43com12 32 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  biimprcd  233  elsnc2g  4010  elpreqprb  4176  reusv2lem2  4619  reusv3  4625  alxfr  4627  reuhypd  4641  opth1  4689  euotd  4716  tz7.2  4837  ordtri1  5475  fvmptdv2  5986  fveqressseq  6041  foco2  6065  fsn  6085  fnsnb  6107  fmptsng  6109  fmptsnd  6110  fconst2g  6143  fnprb  6147  fntpb  6148  funfvima  6165  soisoi  6244  isores3  6251  eusvobj2  6308  ovmpt2dv2  6457  f1opw2  6549  sorpssun  6605  sorpssin  6606  oneqmin  6659  nlimsucg  6696  onzsl  6700  tfinds  6713  funcnvuni  6773  opiota  6879  mpt2sn  6914  suppssov1  6974  suppssfv  6978  brtpos  7008  wfrlem10  7071  wfrlem14  7075  wfrlem15  7076  seqomlem1  7193  seqomlem2  7194  omordi  7293  omord  7295  omwordi  7298  oeeui  7329  nnmordi  7358  nnmord  7359  nnmwordi  7362  nnawordex  7364  nnaordex  7365  nneob  7379  omsmolem  7380  qsss  7450  eroveu  7484  mapsncnv  7544  ralxpmap  7547  elixpsn  7587  ixpsnf1o  7588  boxcutc  7591  pw2f1olem  7702  2pwne  7754  mapxpen  7764  mapunen  7767  php  7782  unxpdomlem2  7803  en1eqsnbi  7828  isfiniteg  7857  fofinf1o  7878  f1opwfi  7904  elfiun  7970  oieu  8080  brwdom2  8114  wdomtr  8116  ixpiunwdom  8132  en3lplem1  8145  suc11reg  8150  inf3lemd  8158  cantnfvalf  8196  cantnflt  8203  cantnfp1lem3  8211  cantnflem2  8221  r1tr  8273  dfac8alem  8486  wdomnumr  8521  isinfcard  8549  aceq3lem  8577  dfac5lem4  8583  dfac5  8585  dfac2  8587  coftr  8729  fin23lem28  8796  fin23lem29  8797  fin1a2lem11  8866  fin1a2lem12  8867  fin1a2lem13  8868  hsmexlem9  8881  axdclem  8975  pwcfsdom  9034  gchdomtri  9080  fpwwe2  9094  gchpwdom  9121  gchhar  9130  addnidpi  9352  nqereu  9380  genpv  9450  genpdm  9453  distrlem5pr  9478  mulid1  9666  ltne  9756  mul02  9837  cnegex  9840  mul0or  10280  negfi  10582  sup2  10593  supaddc  10602  supadd  10603  supmul1  10604  supmul  10607  creur  10631  creui  10632  cju  10633  nnsub  10676  un0addcl  10932  un0mulcl  10933  nn0sub  10949  elz2  10983  zaddcl  11006  suprzcl2  11283  qmulz  11296  qre  11298  qnegcl  11310  xrmax1  11499  xrmin2  11502  max1ALT  11510  xlesubadd  11578  xmulass  11602  xlemul1a  11603  xrsupexmnf  11619  xrinfmexpnf  11620  xrub  11626  iccid  11710  fzsn  11869  fzsuc2  11882  fz1sbc  11899  elfzp12  11902  seqid3  12289  bcval5  12535  bcpasc  12538  hashbnd  12553  hashnnn0genn0  12558  hashprg  12604  hashfzo  12634  wrdl1s1  12788  cats1un  12869  shftlem  13180  replim  13228  absmod0  13415  absz  13423  rlimdm  13664  summolem2  13831  summo  13832  zsum  13833  fsum  13835  fsummulc2  13894  fsumconst  13900  fsum00  13907  incexclem  13943  isumsplit  13947  infcvgaux1i  13964  prodmolem2  14038  prodmo  14039  zprod  14040  fprod  14044  prodsn  14065  prodsnf  14067  fprodconst  14081  ruclem2  14333  fzo0dvdseq  14407  bitsf1ocnv  14467  sadcaddlem  14480  smueqlem  14513  gcdabs1  14547  bezoutlem1  14552  bezoutlem3OLD  14554  bezoutlem4OLD  14555  bezoutlem3  14557  bezoutlem4  14558  dvdsgcd  14560  dvdsmulgcd  14571  lcmgcdeq  14626  lcmf  14655  lcmfunsnlem1  14659  lcmfunsnlem2lem2  14661  dvdsprime  14686  isprm5  14700  coprm  14706  prmdvdsexpr  14718  rpexp  14721  phibndlem  14767  dfphi2  14771  odzdvds  14789  odzdvdsOLD  14795  pythagtriplem1  14815  iserodd  14834  pceulem  14844  pcqmul  14852  pcqcl  14855  pcxcl  14859  pcneg  14872  pcabs  14873  pcgcd1  14875  pcz  14879  pcprmpw2  14880  pcprmpw  14881  pcaddlem  14882  pcadd  14883  pcmpt  14886  pockthg  14899  prmreclem5  14913  4sqlem4  14945  mul4sq  14947  vdwapun  14973  vdwlem2  14981  vdwlem6  14985  vdwlem8  14987  vdwlem13  14992  0ram  15027  ram0  15029  ramcl  15036  cshwsiun  15119  wunress  15238  firest  15380  xpscfv  15517  isssc  15774  pospo  16268  latnlej  16363  gsumval2a  16571  mnd1id  16628  mulgnn0p1  16818  mulgnn0ass  16836  gicsubgen  16991  symg1bas  17086  psgnunilem1  17183  psgnunilem2  17185  mndodcongi  17241  oddvdsnn0  17242  odnncl  17243  oddvds  17245  odeq  17248  odeq1  17260  pgpfi2  17307  sylow2a  17320  sylow2blem3  17323  sylow3lem6  17333  lsmelvalm  17352  lsmsubm  17354  lsmsubg  17355  lsmmod  17374  lsmdisj2  17381  efgmnvl  17413  efgtlen  17425  efgs1b  17435  efgrelexlemb  17449  efgredeu  17451  efgcpbllemb  17454  frgpuptinv  17470  frgpup3lem  17476  qusabl  17552  frgpnabllem1  17558  cyggeninv  17567  cyggenod  17568  cygabl  17574  gsumval3eu  17587  dprdssv  17698  dprdfeq0  17704  dprdsubg  17706  dprddisj2  17721  ablfacrp  17748  pgpfac1lem3  17759  pgpfaclem2  17764  dvreq1  17970  irredn1  17983  drngmul0or  18045  isabvd  18097  abvdom  18115  issrngd  18138  lss1d  18235  lspsneq0  18284  lbspss  18354  lsmcl  18355  lvecvs0or  18380  lspindpi  18404  lidl1el  18491  lpiss  18523  lidldvgen  18528  nzrunit  18540  rrgeq0  18563  domneq0  18570  mplsubrglem  18712  mplmonmul  18737  mplcoe5lem  18740  coe1tmmul2  18918  coe1tmmul  18919  pf1ind  18992  qsssubdrg  19076  zringlpirlem1  19102  znfld  19180  znunit  19183  znrrg  19185  cygznlem3  19189  frgpcyg  19193  psgnghm  19197  ipeq0  19254  cssincl  19300  lsmcss  19304  obselocv  19340  dsmmacl  19353  dsmmlss  19356  mat1dimelbas  19545  mdetralt  19682  mdetunilem2  19687  mdetunilem7  19692  mdetunilem9  19694  maducoeval2  19714  chpscmat  19915  chfacfscmulgsum  19933  chfacfpmmulgsum  19937  istopon  19989  eltg3  20026  tgidm  20045  clsval2  20114  opncldf1  20149  restbas  20223  tgrest  20224  restcld  20237  restcldr  20239  restcls  20246  restntr  20247  ordtbas2  20256  ordtbas  20257  ordtrest2lem  20268  ordtrest2  20269  pnfnei  20285  mnfnei  20286  tgcn  20317  cnconst  20349  cnindis  20357  lmss  20363  ordtt1  20444  discmp  20462  1stcrest  20517  2ndcdisj  20520  cldllycmp  20559  txbas  20631  ptpjpre1  20635  ptuni2  20640  ptbasin  20641  ptbasfi  20645  ptopn2  20648  txbasval  20670  ptpjopn  20676  ptclsg  20679  dfac14lem  20681  xkoccn  20683  ptcnp  20686  upxp  20687  ptrescn  20703  txkgen  20716  xkoptsub  20718  xkopt  20719  xkoco1cn  20721  xkoco2cn  20722  xkococn  20724  xkoinjcn  20751  ordthmeolem  20865  ptuncnv  20871  nrmhaus  20890  fbssint  20902  fbfinnfr  20905  fbasrn  20948  isufil2  20972  filufint  20984  rnelfm  21017  fmfnfmlem2  21019  fmfnfmlem3  21020  fmfnfmlem4  21021  fmfnfm  21022  flimtopon  21034  flimclslem  21048  fclstopon  21076  fclscf  21089  flimfnfcls  21092  alexsublem  21108  alexsubALTlem3  21113  alexsubALTlem4  21114  ptcmplem2  21117  tmdgsum2  21160  symgtgp  21165  cldsubg  21174  qustgplem  21184  tgptsmscld  21214  tsmsxplem1  21216  imasdsf1olem  21437  blssps  21488  blss  21489  stdbdxmet  21579  methaus  21584  metrest  21588  nrginvrcn  21743  nmoeq0  21806  blssioo  21862  xrtgioo  21873  xrsxmet  21876  reconnlem1  21893  reconnlem2  21894  xrge0tsms  21901  elcncf1di  21976  iccpnfcnv  22021  evth  22036  lebnumlem1  22038  lebnumlem2  22039  lebnumlem3  22040  lebnumlem1OLD  22041  lebnumlem2OLD  22042  lebnumlem3OLD  22043  nmoleub3  22182  minveclem3b  22419  minveclem3bOLD  22431  ivthlem2  22452  ivthlem3  22453  elovolm  22477  ovolmge0  22479  ovoliun  22507  ovolicc2lem3  22521  ovolicc2  22525  voliunlem3  22554  dyaddisj  22603  dyadmax  22605  opnmblALT  22610  ismbfd  22645  ismbf2d  22646  mbfimaopnlem  22660  mbfimaopn2  22662  i1fmullem  22701  i1fres  22712  itg1climres  22721  mbfi1fseqlem4  22725  itg2lcl  22734  itgsplitioo  22844  ellimc2  22881  rolle  22991  dvlip  22994  dvge0  23007  dvne0  23012  lhop1lem  23014  tdeglem4  23058  degltlem1  23070  deg1nn0clb  23088  deg1lt0  23089  dvdsq1p  23160  ply1rem  23163  fta1g  23167  elply2  23199  plyf  23201  ne0p  23210  plyeq0lem  23213  plypf1  23215  0dgrb  23249  coe1termlem  23261  dgrcolem2  23277  plymul0or  23283  plyrem  23307  fta1  23310  quotcan  23311  aalioulem3  23339  eff1olem  23546  lognegb  23588  eflogeq  23600  argregt0  23608  argrege0  23609  tanarg  23617  cxpexp  23662  cxpeq0  23672  mulcxp  23679  cxpeq  23746  atans2  23906  scvxcvx  23960  dmgmaddn0  23997  isppw2  24091  vmappw  24092  vmacl  24094  efvmacl  24096  isnsqf  24111  mumullem2  24156  sqff1o  24158  dvdsppwf1o  24164  ppiublem1  24179  vmalelog  24182  chtublem  24188  fsumvma  24190  perfectlem2  24207  perfect  24208  bposlem1  24261  lgsmod  24298  lgsne0  24310  lgsdirnn0  24316  lgsqr  24323  lgsdchr  24325  lgseisenlem2  24327  lgsquadlem1  24331  lgsquadlem2  24332  2sqlem2  24341  mul2sq  24342  2sqlem7  24347  dchrisum0fno1  24398  pntrsumbnd2  24454  ostthlem1  24514  ostth2lem2  24521  ostth3  24525  ostth  24526  colinearalg  24989  axpasch  25020  axlowdimlem16  25036  axlowdimlem17  25037  axlowdim  25040  axcontlem2  25044  axcontlem4  25046  axcontlem7  25049  usgraexmplef  25177  nbgraf1olem1  25218  nbgraf1olem3  25220  nbgraf1olem5  25222  nb3graprlem2  25229  cusgrasize2inds  25254  wlklenvm1  25309  wlkiswwlksur  25496  wwlknextbi  25502  wwlkextproplem2  25519  clwlkisclwwlklem1  25564  clwwisshclww  25584  erclwwlktr  25592  erclwwlkntr  25604  clwlkfclwwlk1hash  25619  vdgr1a  25683  vdusgra0nedg  25685  usgravd0nedg  25695  0eusgraiff0rgra  25716  rusgraprop2  25719  eupap1  25753  vdn0frgrav2  25800  vdgn0frgrav2  25801  ismndo2  26122  ghgrplem1OLD  26143  nvmul0or  26322  ipasslem5  26525  ipasslem11  26530  hvmul0or  26727  his6  26801  hhssnv  26964  ocsh  26985  ocin  26998  shsidmi  27086  chnlen0  27146  h1de2bi  27256  h1de2ctlem  27257  h1de2ci  27258  spansni  27259  3oalem1  27364  nmcexi  27728  atcveq0  28050  chcv1  28057  cdjreui  28134  cdj3lem2b  28139  xrge0tsmsd  28597  ordtrest2NEWlem  28777  ordtrest2NEW  28778  xrge0iifcnv  28788  esumc  28921  esumpcvgval  28948  ballotlemfc0  29374  ballotlemfcc  29375  bnj145OLD  29584  subfacp1lem4  29955  subfacp1lem5  29956  erdszelem8  29970  sconpi1  30011  cvmsss2  30046  cvmlift2lem12  30086  msubco  30218  msubvrs  30247  sinccvglem  30365  untsucf  30386  dfpo2  30444  dfrdg2  30491  trpred0  30526  frrlem4  30566  colineardim1  30877  btwnconn1lem14  30916  segleantisym  30931  colinbtwnle  30934  outsidele  30948  lineunray  30963  linethru  30969  elicc3  31022  opnregcld  31035  cldregopn  31036  fnejoin2  31074  dissneqlem  31787  icorempt2  31799  relowlssretop  31811  relowlpssretop  31812  finxpsuclem  31834  ptrecube  31985  poimirlem6  31991  poimirlem7  31992  poimirlem16  32001  poimirlem17  32002  poimirlem19  32004  poimirlem20  32005  poimirlem21  32006  poimirlem22  32007  poimirlem23  32008  poimirlem24  32009  poimirlem25  32010  poimirlem26  32011  poimirlem27  32012  poimirlem29  32014  poimirlem30  32015  poimirlem31  32016  poimirlem32  32017  itg2addnclem3  32040  ftc1anclem6  32067  dvasin  32073  unirep  32084  sdclem2  32116  ssbnd  32165  prdsbnd  32170  cntotbnd  32173  heibor1lem  32186  rrnequiv  32212  grpoeqdivid  32224  isdrngo3  32243  crngohomfo  32284  0idl  32303  1idl  32304  divrngidl  32306  smprngopr  32330  prnc  32345  ispridlc  32348  riotaclbgBAD  32571  lshpdisj  32598  lsateln0  32606  lsatcveq0  32643  opnlen0  32799  cmtbr4N  32866  cvrnbtwn2  32886  cvrnbtwn4  32890  atcvreq0  32925  cvlatexch1  32947  exatleN  33014  atlelt  33048  ps-2  33088  llnn0  33126  lplnn0N  33157  islpln2a  33158  lvoln0N  33201  islvol2aN  33202  4at  33223  dalemcea  33270  dalem3  33274  pmapglb2N  33381  pmapglb2xN  33382  cdlema1N  33401  cdlemb  33404  paddasslem17  33446  llnexchb2lem  33478  llnexchb2  33479  lhpat3  33656  ltrnid  33745  trlne  33796  cdlemc4  33805  cdleme11h  33877  cdlemednuN  33911  cdlemg1a  34182  tendoeq2  34386  tendoid0  34437  dva1dim  34597  dib1dim  34778  dihlatat  34950  dochkrshp4  35002  dochkr1  35091  lclkrlem2e  35124  lcfrlem16  35171  lcfrlem28  35183  mapd0  35278  hdmap14lem13  35496  elrfi  35581  mrefg2  35594  eldiophb  35644  eldioph2b  35650  diophin  35660  diophun  35661  rexzrexnn0  35692  eldioph4b  35699  diophren  35701  rencldnfilem  35708  pellexlem6  35723  jm2.19  35893  rmydioph  35914  expdiophlem1  35921  expdioph  35923  lnr2i  36020  lpirlnr  36021  hbtlem2  36028  hbtlem4  36030  hbtlem6  36033  dgrsub2  36039  dgraa0p  36060  rngunsnply  36084  hashgcdlem  36119  radcnvrat  36707  pm14.24  36827  addrcom  36872  afveu  38693  dfafn5b  38701  rlimdmafv  38717  el1fzopredsuc  38760  perfectALTVlem2  38882  perfectALTV  38883  gbopos  38898  gbogt5  38901  gboage9  38903  nnsum4primesodd  38929  nnsum4primesoddALTV  38930  proththdlem  38951  riotaeqimp  39079  lpvtx  39205  uhgrauhgr  39208  usgredgop  39305  uhgrspansubgrlem  39412  uhgrspan1  39425  nbusgredgeu0  39492  nb3grprlem2  39505  cusgrsize2inds  39564  uhgrvd0nedgb  39595  rusgrpropnb  39649  1wlklenvm1  39686  upgr1wlkvtxedg  39704  wlkOnwlk1l  39713  usgr2wlkneq  39788  31wlkdlem6  39906  uhgrauhg  39958  lincellss  40492  lindsrng01  40534  suppdm  40577  nnpw2pb  40671
  Copyright terms: Public domain W3C validator