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  3895  reusv2lem2  4482  reusv3  4488  alxfr  4493  reuhypd  4507  opth1  4553  euotd  4580  tz7.2  4691  ordtri1  4739  xpsspw  4940  fvmptdv2  5775  foco2  5851  fsn  5868  fnsnb  5885  fmptsng  5887  fconst2g  5919  fnprb  5923  fnprOLD  5924  funfvima  5939  soisoi  6006  isores3  6013  eusvobj2  6072  ovmpt2dv2  6213  f1opw2  6302  suppssfvOLD  6305  suppssov1OLD  6306  sorpssun  6356  sorpssin  6357  oneqmin  6405  nlimsucg  6442  onzsl  6446  tfinds  6459  funcnvuni  6519  opiota  6622  suppssov1  6710  suppssfv  6714  brtpos  6743  seqomlem1  6891  seqomlem2  6892  omordi  6993  omord  6995  omwordi  6998  oeeui  7029  nnmordi  7058  nnmord  7059  nnmwordi  7062  nnawordex  7064  nnaordex  7065  nneob  7079  omsmolem  7080  qsss  7149  eroveu  7183  th3qlem1  7194  mapsncnv  7247  ralxpmap  7250  elixpsn  7290  ixpsnf1o  7291  boxcutc  7294  pw2f1olem  7403  2pwne  7455  mapxpen  7465  mapunen  7468  php  7483  unxpdomlem2  7506  isfiniteg  7560  fofinf1o  7580  f1opwfi  7603  elfiun  7668  oieu  7741  brwdom2  7776  wdomtr  7778  ixpiunwdom  7794  en3lplem1  7808  suc11reg  7813  inf3lemd  7821  cantnfvalf  7861  cantnflt  7868  cantnfp1lem3  7876  cantnflem2  7886  cantnfltOLD  7898  cantnfp1lem3OLD  7902  r1tr  7971  dfac8alem  8187  wdomnumr  8222  isinfcard  8250  aceq3lem  8278  dfac5lem4  8284  dfac5  8286  dfac2  8288  coftr  8430  fin23lem28  8497  fin23lem29  8498  fin1a2lem11  8567  fin1a2lem12  8568  fin1a2lem13  8569  hsmexlem9  8582  axdclem  8676  pwcfsdom  8735  gchdomtri  8783  fpwwe2  8797  gchpwdom  8824  gchhar  8833  addnidpi  9057  nqereu  9085  genpv  9155  genpdm  9158  distrlem5pr  9183  mulid1  9370  ltne  9458  mul02  9534  cnegex  9537  mul0or  9963  sup2  10273  supmul1  10282  supmul  10285  creur  10303  creui  10304  cju  10305  nnsub  10347  un0addcl  10600  un0mulcl  10601  nn0sub  10617  elz2  10650  zaddcl  10672  suprzcl2  10932  qmulz  10943  qre  10945  qnegcl  10957  xrmax1  11134  xrmin2  11137  max1ALT  11145  xlesubadd  11213  xmulass  11237  xlemul1a  11238  xrsupexmnf  11254  xrinfmexpnf  11255  xrub  11261  iccid  11332  fzsn  11486  fzsuc2  11498  fz1sbc  11519  elfzp12  11522  fzm1  11523  seqid3  11833  bcval5  12077  bcpasc  12080  hashbnd  12092  hashnnn0genn0  12097  hashprg  12138  hashfzo  12173  wrdl1s1  12284  cats1un  12353  shftlem  12540  replim  12588  absmod0  12775  absz  12783  rlimdm  13012  summolem2  13176  summo  13177  zsum  13178  fsum  13180  fsummulc2  13233  fsumconst  13239  fsum00  13243  incexclem  13281  isumsplit  13285  infcvgaux1i  13301  ruclem2  13496  fzo0dvdseq  13568  bitsf1ocnv  13622  sadcaddlem  13635  smueqlem  13668  gcdabs1  13700  bezoutlem1  13704  bezoutlem3  13706  bezoutlem4  13707  dvdsgcd  13709  dvdsmulgcd  13720  dvdsprime  13758  coprm  13768  isprm5  13780  prmdvdsexpr  13784  rpexp  13788  phibndlem  13827  dfphi2  13831  odzdvds  13849  pythagtriplem1  13865  iserodd  13884  pceulem  13894  pcqmul  13902  pcqcl  13905  pcxcl  13909  pcneg  13922  pcabs  13923  pcgcd1  13925  pcz  13929  pcprmpw2  13930  pcprmpw  13931  pcaddlem  13932  pcadd  13933  pcmpt  13936  pockthg  13949  prmreclem5  13963  4sqlem4  13995  mul4sq  13997  vdwapun  14017  vdwlem2  14025  vdwlem6  14029  vdwlem8  14031  vdwlem13  14036  0ram  14063  ram0  14065  ramcl  14072  cshwsiun  14108  wunress  14219  firest  14353  xpscfv  14482  isssc  14715  pospo  15125  latnlej  15220  gsumval2a  15491  mulgnn0p1  15617  mulgnn0ass  15635  gicsubgen  15785  symg1bas  15880  psgnunilem1  15978  psgnunilem2  15980  mndodcongi  16025  oddvdsnn0  16026  odnncl  16027  oddvds  16029  odeq  16032  odeq1  16040  pgpfi2  16084  sylow2a  16097  sylow2blem3  16100  sylow3lem6  16110  lsmelvalm  16129  lsmsubm  16131  lsmsubg  16132  lsmmod  16151  lsmdisj2  16158  efgmnvl  16190  efgtlen  16202  efgs1b  16212  efgrelexlemb  16226  efgredeu  16228  efgcpbllemb  16231  frgpuptinv  16247  frgpup3lem  16253  divsabl  16326  frgpnabllem1  16330  cyggeninv  16339  cyggenod  16340  cygabl  16346  gsumval3eu  16360  dprdssv  16479  dprdfeq0  16485  dprdfeq0OLD  16492  dprdsubg  16494  dprddisj2  16510  dprddisj2OLD  16511  ablfacrp  16540  pgpfac1lem3  16551  pgpfaclem2  16556  dvreq1  16718  irredn1  16731  drngmul0or  16776  isabvd  16828  abvdom  16846  issrngd  16869  lss1d  16965  lspsneq0  17014  lbspss  17084  lsmcl  17085  lvecvs0or  17110  lspindpi  17134  lidl1el  17221  lpiss  17253  lidldvgen  17258  nzrunit  17269  rrgeq0  17282  domneq0  17290  mplsubrglem  17450  mplsubrglemOLD  17451  mplmonmul  17476  coe1tmmul2  17626  coe1tmmul  17627  qsssubdrg  17715  zringlpirlem1  17744  zlpirlem1  17749  znfld  17834  znunit  17837  znrrg  17839  cygznlem3  17843  frgpcyg  17847  psgnghm  17851  ipeq0  17908  cssincl  17954  lsmcss  17958  obselocv  17994  dsmmacl  18007  dsmmlss  18010  mdetralt  18255  mdetunilem2  18260  mdetunilem7  18265  mdetunilem9  18267  maducoeval2  18287  istopon  18371  eltg3  18408  tgidm  18426  clsval2  18495  opncldf1  18529  restbas  18603  tgrest  18604  restcld  18617  restcldr  18619  restcls  18626  restntr  18627  ordtbas2  18636  ordtbas  18637  ordtrest2lem  18648  ordtrest2  18649  pnfnei  18665  mnfnei  18666  tgcn  18697  cnconst  18729  cnindis  18737  lmss  18743  ordtt1  18824  discmp  18842  1stcrest  18898  2ndcdisj  18901  cldllycmp  18940  txbas  18981  ptpjpre1  18985  ptuni2  18990  ptbasin  18991  ptbasfi  18995  ptopn2  18998  txbasval  19020  ptpjopn  19026  ptclsg  19029  dfac14lem  19031  xkoccn  19033  ptcnp  19036  upxp  19037  ptrescn  19053  txkgen  19066  xkoptsub  19068  xkopt  19069  xkoco1cn  19071  xkoco2cn  19072  xkococn  19074  xkoinjcn  19101  ordthmeolem  19215  ptuncnv  19221  nrmhaus  19240  fbssint  19252  fbfinnfr  19255  fbasrn  19298  isufil2  19322  filufint  19334  rnelfm  19367  fmfnfmlem2  19369  fmfnfmlem3  19370  fmfnfmlem4  19371  fmfnfm  19372  flimtopon  19384  flimclslem  19398  fclstopon  19426  fclscf  19439  flimfnfcls  19442  alexsublem  19457  alexsubALTlem3  19462  alexsubALTlem4  19463  ptcmplem2  19466  tmdgsum2  19508  symgtgp  19513  cldsubg  19522  divstgplem  19532  tgptsmscld  19566  tsmsxplem1  19568  imasdsf1olem  19789  blssps  19840  blss  19841  stdbdxmet  19931  methaus  19936  metrest  19940  nrginvrcn  20113  nmoeq0  20156  blssioo  20213  xrtgioo  20224  xrsxmet  20227  reconnlem1  20244  reconnlem2  20245  xrge0tsms  20252  elcncf1di  20312  iccpnfcnv  20357  evth  20372  lebnumlem1  20374  lebnumlem2  20375  lebnumlem3  20376  nmoleub3  20515  minveclem3b  20756  ivthlem2  20777  ivthlem3  20778  elovolm  20799  ovolmge0  20801  ovoliun  20829  ovolicc2lem3  20843  ovolicc2  20846  voliunlem3  20874  dyaddisj  20917  dyadmax  20919  opnmblALT  20924  ismbfd  20959  ismbf2d  20960  mbfimaopnlem  20974  mbfimaopn2  20976  i1fmullem  21013  i1fres  21024  itg1climres  21033  mbfi1fseqlem4  21037  itg2lcl  21046  itgsplitioo  21156  ellimc2  21193  rolle  21303  dvlip  21306  dvge0  21319  dvne0  21324  lhop1lem  21326  pf1ind  21405  tdeglem4  21413  degltlem1  21427  deg1nn0clb  21445  deg1lt0  21446  dvdsq1p  21516  ply1rem  21519  fta1g  21523  elply2  21548  plyf  21550  ne0p  21559  plyeq0lem  21562  plypf1  21564  0dgrb  21598  coe1termlem  21609  dgrcolem2  21625  plymul0or  21631  plyrem  21655  fta1  21658  quotcan  21659  aalioulem3  21684  eff1olem  21888  lognegb  21922  eflogeq  21934  argregt0  21943  argrege0  21944  tanarg  21952  cxpexp  21997  cxpeq0  22007  mulcxp  22014  cxpeq  22079  atans2  22210  scvxcvx  22263  isppw2  22337  vmappw  22338  vmacl  22340  efvmacl  22342  isnsqf  22357  mumullem2  22402  sqff1o  22404  dvdsppwf1o  22410  ppiublem1  22425  vmalelog  22428  chtublem  22434  fsumvma  22436  perfectlem2  22453  perfect  22454  bposlem1  22507  lgsmod  22544  lgsne0  22556  lgsdirnn0  22562  lgsqr  22569  lgsdchr  22571  lgseisenlem2  22573  lgsquadlem1  22577  lgsquadlem2  22578  2sqlem2  22587  mul2sq  22588  2sqlem7  22593  dchrisum0fno1  22644  pntrsumbnd2  22700  ostthlem1  22760  ostth2lem2  22767  ostth3  22771  ostth  22772  colinearalg  22978  axpasch  23009  axlowdimlem16  23025  axlowdimlem17  23026  axlowdim  23029  axcontlem2  23033  axcontlem4  23035  axcontlem7  23038  usgraexmpl  23141  nbgraf1olem1  23172  nbgraf1olem3  23174  nbgraf1olem5  23176  nb3graprlem2  23182  cusgrasize2inds  23207  vdgr1a  23398  vdusgra0nedg  23400  usgravd0nedg  23404  eupap1  23419  ismndo2  23654  ghgrplem1  23675  rngosn4  23736  nvmul0or  23854  ipasslem5  24057  ipasslem11  24062  hvmul0or  24249  his6  24323  hhssnv  24487  ocsh  24508  ocin  24521  shsidmi  24609  chnlen0  24669  h1de2bi  24779  h1de2ctlem  24780  h1de2ci  24781  spansni  24782  3oalem1  24887  nmcexi  25252  atcveq0  25574  chcv1  25581  cdjreui  25658  cdj3lem2b  25663  xrge0tsmsd  26105  ordtrest2NEWlem  26205  ordtrest2NEW  26206  xrge0iifcnv  26216  esumc  26358  esumpcvgval  26380  ballotlemfc0  26722  ballotlemfcc  26723  dmgmaddn0  26856  subfacp1lem4  26918  subfacp1lem5  26919  erdszelem8  26933  sconpi1  26975  cvmsss2  27010  cvmlift2lem12  27050  sinccvglem  27163  untsucf  27207  prodmolem2  27294  prodmo  27295  zprod  27296  fprod  27300  prodsn  27319  fprodconst  27335  dfpo2  27411  dfrdg2  27455  trpred0  27546  wfrlem10  27579  wfrlem14  27583  wfrlem15  27584  frrlem4  27617  colineardim1  27938  btwnconn1lem14  27977  segleantisym  27992  colinbtwnle  27995  outsidele  28009  lineunray  28024  linethru  28030  supaddc  28258  supadd  28259  itg2addnclem3  28286  ftc1anclem6  28313  dvasin  28321  elicc3  28353  opnregcld  28366  cldregopn  28367  fnejoin2  28431  unirep  28447  sdclem2  28479  ssbnd  28528  prdsbnd  28533  cntotbnd  28536  heibor1lem  28549  rrnequiv  28575  grpoeqdivid  28587  isdrngo3  28606  crngohomfo  28647  0idl  28666  1idl  28667  divrngidl  28669  smprngopr  28693  prnc  28708  ispridlc  28711  elrfi  28872  mrefg2  28885  eldiophb  28937  eldioph2b  28943  diophin  28953  diophun  28954  rexzrexnn0  28984  eldioph4b  28992  diophren  28994  rencldnfilem  29001  pellexlem6  29017  jm2.19  29184  rmydioph  29205  expdiophlem1  29212  expdioph  29214  lnr2i  29314  lpirlnr  29315  hbtlem2  29322  hbtlem4  29324  hbtlem6  29327  dgrsub2  29333  dgraa0p  29348  rngunsnply  29372  hashgcdlem  29407  pm14.24  29528  addrcom  29573  afveu  29902  dfafn5b  29910  rlimdmafv  29926  wlklenfislenpm1  30127  wlklniswwlkn2  30177  wlkiswwlksur  30194  wwlknextbi  30200  clwlkisclwwlklem1  30292  clwwisshclww  30314  erclwwlktr  30328  erclwwlkntr  30344  clwlkfclwwlk1hash  30358  0eusgraiff0rgra  30395  rusgraprop2  30397  wwlkextproplem2  30404  vdn0frgrav2  30459  vdgn0frgrav2  30460  fmptsnd  30564  mpt2sn  30565  lincellss  30666  lindsrng01  30708  bnj145OLD  31417  riotaclbgBAD  32175  riotaclbBAD  32176  lshpdisj  32202  lsateln0  32210  lsatcveq0  32247  opnlen0  32403  cmtbr4N  32470  cvrnbtwn2  32490  cvrnbtwn4  32494  atcvreq0  32529  cvlatexch1  32551  exatleN  32618  atlelt  32652  ps-2  32692  llnn0  32730  lplnn0N  32761  islpln2a  32762  lvoln0N  32805  islvol2aN  32806  4at  32827  dalemcea  32874  dalem3  32878  pmapglb2N  32985  pmapglb2xN  32986  cdlema1N  33005  cdlemb  33008  paddasslem17  33050  llnexchb2lem  33082  llnexchb2  33083  lhpat3  33260  ltrnid  33349  trlne  33399  cdlemc4  33408  cdleme11h  33480  cdlemednuN  33514  cdlemg1a  33784  tendoeq2  33988  tendoid0  34039  dva1dim  34199  dib1dim  34380  dihlatat  34552  dochkrshp4  34604  dochkr1  34693  lclkrlem2e  34726  lcfrlem16  34773  lcfrlem28  34785  mapd0  34880  hdmap14lem13  35098
  Copyright terms: Public domain W3C validator