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  4032  reusv2lem2  4627  reusv3  4633  alxfr  4635  reuhypd  4649  opth1  4695  euotd  4722  tz7.2  4838  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  6990  wfrlem10  7053  wfrlem14  7057  wfrlem15  7058  seqomlem1  7175  seqomlem2  7176  omordi  7275  omord  7277  omwordi  7280  oeeui  7311  nnmordi  7340  nnmord  7341  nnmwordi  7344  nnawordex  7346  nnaordex  7347  nneob  7361  omsmolem  7362  qsss  7432  eroveu  7466  mapsncnv  7526  ralxpmap  7529  elixpsn  7569  ixpsnf1o  7570  boxcutc  7573  pw2f1olem  7682  2pwne  7734  mapxpen  7744  mapunen  7747  php  7762  unxpdomlem2  7783  en1eqsnbi  7808  isfiniteg  7837  fofinf1o  7858  f1opwfi  7884  elfiun  7950  oieu  8054  brwdom2  8088  wdomtr  8090  ixpiunwdom  8106  en3lplem1  8119  suc11reg  8124  inf3lemd  8132  cantnfvalf  8169  cantnflt  8176  cantnfp1lem3  8184  cantnflem2  8194  r1tr  8246  dfac8alem  8458  wdomnumr  8493  isinfcard  8521  aceq3lem  8549  dfac5lem4  8555  dfac5  8557  dfac2  8559  coftr  8701  fin23lem28  8768  fin23lem29  8769  fin1a2lem11  8838  fin1a2lem12  8839  fin1a2lem13  8840  hsmexlem9  8853  axdclem  8947  pwcfsdom  9006  gchdomtri  9053  fpwwe2  9067  gchpwdom  9094  gchhar  9103  addnidpi  9325  nqereu  9353  genpv  9423  genpdm  9426  distrlem5pr  9451  mulid1  9639  ltne  9729  mul02  9810  cnegex  9813  mul0or  10251  negfi  10554  sup2  10565  supaddc  10574  supadd  10575  supmul1  10576  supmul  10579  creur  10603  creui  10604  cju  10605  nnsub  10648  un0addcl  10903  un0mulcl  10904  nn0sub  10920  elz2  10954  zaddcl  10977  suprzcl2  11254  qmulz  11267  qre  11269  qnegcl  11281  xrmax1  11470  xrmin2  11473  max1ALT  11481  xlesubadd  11549  xmulass  11573  xlemul1a  11574  xrsupexmnf  11590  xrinfmexpnf  11591  xrub  11597  iccid  11681  fzsn  11838  fzsuc2  11851  fz1sbc  11868  elfzp12  11871  seqid3  12254  bcval5  12500  bcpasc  12503  hashbnd  12518  hashnnn0genn0  12523  hashprg  12569  hashfzo  12596  wrdl1s1  12736  cats1un  12817  shftlem  13110  replim  13158  absmod0  13345  absz  13353  rlimdm  13593  summolem2  13760  summo  13761  zsum  13762  fsum  13764  fsummulc2  13823  fsumconst  13829  fsum00  13836  incexclem  13872  isumsplit  13876  infcvgaux1i  13893  prodmolem2  13967  prodmo  13968  zprod  13969  fprod  13973  prodsn  13994  prodsnf  13996  fprodconst  14010  ruclem2  14262  fzo0dvdseq  14336  bitsf1ocnv  14392  sadcaddlem  14405  smueqlem  14438  gcdabs1  14472  bezoutlem1  14477  bezoutlem3  14479  bezoutlem4  14480  dvdsgcd  14482  dvdsmulgcd  14493  lcmgcdeq  14548  lcmf  14577  lcmfunsnlem1  14581  lcmfunsnlem2lem2  14583  dvdsprime  14608  isprm5  14622  coprm  14628  prmdvdsexpr  14640  rpexp  14643  phibndlem  14687  dfphi2  14691  odzdvds  14709  pythagtriplem1  14729  iserodd  14748  pceulem  14758  pcqmul  14766  pcqcl  14769  pcxcl  14773  pcneg  14786  pcabs  14787  pcgcd1  14789  pcz  14793  pcprmpw2  14794  pcprmpw  14795  pcaddlem  14796  pcadd  14797  pcmpt  14800  pockthg  14813  prmreclem5  14827  4sqlem4  14859  mul4sq  14861  vdwapun  14887  vdwlem2  14895  vdwlem6  14899  vdwlem8  14901  vdwlem13  14906  0ram  14941  ram0  14943  ramcl  14950  cshwsiun  15033  wunress  15151  firest  15290  xpscfv  15419  isssc  15676  pospo  16170  latnlej  16265  gsumval2a  16473  mnd1id  16530  mulgnn0p1  16720  mulgnn0ass  16738  gicsubgen  16893  symg1bas  16988  psgnunilem1  17085  psgnunilem2  17087  mndodcongi  17134  oddvdsnn0  17135  odnncl  17136  oddvds  17138  odeq  17141  odeq1  17149  pgpfi2  17193  sylow2a  17206  sylow2blem3  17209  sylow3lem6  17219  lsmelvalm  17238  lsmsubm  17240  lsmsubg  17241  lsmmod  17260  lsmdisj2  17267  efgmnvl  17299  efgtlen  17311  efgs1b  17321  efgrelexlemb  17335  efgredeu  17337  efgcpbllemb  17340  frgpuptinv  17356  frgpup3lem  17362  qusabl  17438  frgpnabllem1  17444  cyggeninv  17453  cyggenod  17454  cygabl  17460  gsumval3eu  17473  dprdssv  17584  dprdfeq0  17590  dprdsubg  17592  dprddisj2  17607  ablfacrp  17634  pgpfac1lem3  17645  pgpfaclem2  17650  dvreq1  17856  irredn1  17869  drngmul0or  17931  isabvd  17983  abvdom  18001  issrngd  18024  lss1d  18121  lspsneq0  18170  lbspss  18240  lsmcl  18241  lvecvs0or  18266  lspindpi  18290  lidl1el  18377  lpiss  18409  lidldvgen  18414  nzrunit  18426  rrgeq0  18449  domneq0  18456  mplsubrglem  18598  mplmonmul  18623  mplcoe5lem  18626  coe1tmmul2  18804  coe1tmmul  18805  pf1ind  18878  qsssubdrg  18962  zringlpirlem1  18987  znfld  19062  znunit  19065  znrrg  19067  cygznlem3  19071  frgpcyg  19075  psgnghm  19079  ipeq0  19136  cssincl  19182  lsmcss  19186  obselocv  19222  dsmmacl  19235  dsmmlss  19238  mat1dimelbas  19427  mdetralt  19564  mdetunilem2  19569  mdetunilem7  19574  mdetunilem9  19576  maducoeval2  19596  chpscmat  19797  chfacfscmulgsum  19815  chfacfpmmulgsum  19819  istopon  19871  eltg3  19908  tgidm  19927  clsval2  19996  opncldf1  20031  restbas  20105  tgrest  20106  restcld  20119  restcldr  20121  restcls  20128  restntr  20129  ordtbas2  20138  ordtbas  20139  ordtrest2lem  20150  ordtrest2  20151  pnfnei  20167  mnfnei  20168  tgcn  20199  cnconst  20231  cnindis  20239  lmss  20245  ordtt1  20326  discmp  20344  1stcrest  20399  2ndcdisj  20402  cldllycmp  20441  txbas  20513  ptpjpre1  20517  ptuni2  20522  ptbasin  20523  ptbasfi  20527  ptopn2  20530  txbasval  20552  ptpjopn  20558  ptclsg  20561  dfac14lem  20563  xkoccn  20565  ptcnp  20568  upxp  20569  ptrescn  20585  txkgen  20598  xkoptsub  20600  xkopt  20601  xkoco1cn  20603  xkoco2cn  20604  xkococn  20606  xkoinjcn  20633  ordthmeolem  20747  ptuncnv  20753  nrmhaus  20772  fbssint  20784  fbfinnfr  20787  fbasrn  20830  isufil2  20854  filufint  20866  rnelfm  20899  fmfnfmlem2  20901  fmfnfmlem3  20902  fmfnfmlem4  20903  fmfnfm  20904  flimtopon  20916  flimclslem  20930  fclstopon  20958  fclscf  20971  flimfnfcls  20974  alexsublem  20990  alexsubALTlem3  20995  alexsubALTlem4  20996  ptcmplem2  20999  tmdgsum2  21042  symgtgp  21047  cldsubg  21056  qustgplem  21066  tgptsmscld  21096  tsmsxplem1  21098  imasdsf1olem  21319  blssps  21370  blss  21371  stdbdxmet  21461  methaus  21466  metrest  21470  nrginvrcn  21625  nmoeq0  21668  blssioo  21724  xrtgioo  21735  xrsxmet  21738  reconnlem1  21755  reconnlem2  21756  xrge0tsms  21763  elcncf1di  21823  iccpnfcnv  21868  evth  21883  lebnumlem1  21885  lebnumlem2  21886  lebnumlem3  21887  nmoleub3  22026  minveclem3b  22263  ivthlem2  22284  ivthlem3  22285  elovolm  22306  ovolmge0  22308  ovoliun  22336  ovolicc2lem3  22350  ovolicc2  22353  voliunlem3  22382  dyaddisj  22431  dyadmax  22433  opnmblALT  22438  ismbfd  22473  ismbf2d  22474  mbfimaopnlem  22488  mbfimaopn2  22490  i1fmullem  22529  i1fres  22540  itg1climres  22549  mbfi1fseqlem4  22553  itg2lcl  22562  itgsplitioo  22672  ellimc2  22709  rolle  22819  dvlip  22822  dvge0  22835  dvne0  22840  lhop1lem  22842  tdeglem4  22886  degltlem1  22898  deg1nn0clb  22916  deg1lt0  22917  dvdsq1p  22986  ply1rem  22989  fta1g  22993  elply2  23018  plyf  23020  ne0p  23029  plyeq0lem  23032  plypf1  23034  0dgrb  23068  coe1termlem  23080  dgrcolem2  23096  plymul0or  23102  plyrem  23126  fta1  23129  quotcan  23130  aalioulem3  23155  eff1olem  23362  lognegb  23404  eflogeq  23416  argregt0  23424  argrege0  23425  tanarg  23433  cxpexp  23478  cxpeq0  23488  mulcxp  23495  cxpeq  23562  atans2  23722  scvxcvx  23776  dmgmaddn0  23813  isppw2  23905  vmappw  23906  vmacl  23908  efvmacl  23910  isnsqf  23925  mumullem2  23970  sqff1o  23972  dvdsppwf1o  23978  ppiublem1  23993  vmalelog  23996  chtublem  24002  fsumvma  24004  perfectlem2  24021  perfect  24022  bposlem1  24075  lgsmod  24112  lgsne0  24124  lgsdirnn0  24130  lgsqr  24137  lgsdchr  24139  lgseisenlem2  24141  lgsquadlem1  24145  lgsquadlem2  24146  2sqlem2  24155  mul2sq  24156  2sqlem7  24161  dchrisum0fno1  24212  pntrsumbnd2  24268  ostthlem1  24328  ostth2lem2  24335  ostth3  24339  ostth  24340  colinearalg  24786  axpasch  24817  axlowdimlem16  24833  axlowdimlem17  24834  axlowdim  24837  axcontlem2  24841  axcontlem4  24843  axcontlem7  24846  usgraexmpl  24974  nbgraf1olem1  25014  nbgraf1olem3  25016  nbgraf1olem5  25018  nb3graprlem2  25025  cusgrasize2inds  25050  wlklenvm1  25105  wlkiswwlksur  25292  wwlknextbi  25298  wwlkextproplem2  25315  clwlkisclwwlklem1  25360  clwwisshclww  25380  erclwwlktr  25388  erclwwlkntr  25400  clwlkfclwwlk1hash  25415  vdgr1a  25479  vdusgra0nedg  25481  usgravd0nedg  25491  0eusgraiff0rgra  25512  rusgraprop2  25515  eupap1  25549  vdn0frgrav2  25596  vdgn0frgrav2  25597  ismndo2  25918  ghgrplem1OLD  25939  nvmul0or  26118  ipasslem5  26321  ipasslem11  26326  hvmul0or  26513  his6  26587  hhssnv  26750  ocsh  26771  ocin  26784  shsidmi  26872  chnlen0  26932  h1de2bi  27042  h1de2ctlem  27043  h1de2ci  27044  spansni  27045  3oalem1  27150  nmcexi  27514  atcveq0  27836  chcv1  27843  cdjreui  27920  cdj3lem2b  27925  xrge0tsmsd  28387  ordtrest2NEWlem  28567  ordtrest2NEW  28568  xrge0iifcnv  28578  esumc  28711  esumpcvgval  28738  ballotlemfc0  29151  ballotlemfcc  29152  bnj145OLD  29323  subfacp1lem4  29694  subfacp1lem5  29695  erdszelem8  29709  sconpi1  29750  cvmsss2  29785  cvmlift2lem12  29825  msubco  29957  msubvrs  29986  sinccvglem  30104  untsucf  30125  dfpo2  30182  dfrdg2  30229  trpred0  30264  frrlem4  30304  colineardim1  30613  btwnconn1lem14  30652  segleantisym  30667  colinbtwnle  30670  outsidele  30684  lineunray  30699  linethru  30705  elicc3  30758  opnregcld  30771  cldregopn  30772  fnejoin2  30810  dissneqlem  31476  icorempt2  31488  relowlssretop  31500  relowlpssretop  31501  ptrecube  31643  poimirlem6  31649  poimirlem7  31650  poimirlem16  31659  poimirlem17  31660  poimirlem19  31662  poimirlem20  31663  poimirlem21  31664  poimirlem22  31665  poimirlem23  31666  poimirlem24  31667  poimirlem25  31668  poimirlem26  31669  poimirlem27  31670  poimirlem29  31672  poimirlem30  31673  poimirlem31  31674  poimirlem32  31675  itg2addnclem3  31698  ftc1anclem6  31725  dvasin  31731  unirep  31742  sdclem2  31774  ssbnd  31823  prdsbnd  31828  cntotbnd  31831  heibor1lem  31844  rrnequiv  31870  grpoeqdivid  31882  isdrngo3  31901  crngohomfo  31942  0idl  31961  1idl  31962  divrngidl  31964  smprngopr  31988  prnc  32003  ispridlc  32006  riotaclbgBAD  32234  lshpdisj  32261  lsateln0  32269  lsatcveq0  32306  opnlen0  32462  cmtbr4N  32529  cvrnbtwn2  32549  cvrnbtwn4  32553  atcvreq0  32588  cvlatexch1  32610  exatleN  32677  atlelt  32711  ps-2  32751  llnn0  32789  lplnn0N  32820  islpln2a  32821  lvoln0N  32864  islvol2aN  32865  4at  32886  dalemcea  32933  dalem3  32937  pmapglb2N  33044  pmapglb2xN  33045  cdlema1N  33064  cdlemb  33067  paddasslem17  33109  llnexchb2lem  33141  llnexchb2  33142  lhpat3  33319  ltrnid  33408  trlne  33459  cdlemc4  33468  cdleme11h  33540  cdlemednuN  33574  cdlemg1a  33845  tendoeq2  34049  tendoid0  34100  dva1dim  34260  dib1dim  34441  dihlatat  34613  dochkrshp4  34665  dochkr1  34754  lclkrlem2e  34787  lcfrlem16  34834  lcfrlem28  34846  mapd0  34941  hdmap14lem13  35159  elrfi  35244  mrefg2  35257  eldiophb  35307  eldioph2b  35313  diophin  35323  diophun  35324  rexzrexnn0  35355  eldioph4b  35362  diophren  35364  rencldnfilem  35371  pellexlem6  35387  jm2.19  35553  rmydioph  35574  expdiophlem1  35581  expdioph  35583  lnr2i  35680  lpirlnr  35681  hbtlem2  35688  hbtlem4  35690  hbtlem6  35693  dgrsub2  35699  dgraa0p  35713  rngunsnply  35737  hashgcdlem  35772  radcnvrat  36299  pm14.24  36419  addrcom  36464  afveu  38044  dfafn5b  38052  rlimdmafv  38068  el1fzopredsuc  38111  perfectALTVlem2  38233  perfectALTV  38234  gbopos  38249  gbogt5  38252  gboage9  38254  nnsum4primesodd  38280  nnsum4primesoddALTV  38281  proththdlem  38302  uhgrauhg  38442  lincellss  38978  lindsrng01  39020  suppdm  39063  nnpw2pb  39158
  Copyright terms: Public domain W3C validator