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

Theorem syl5ibrcom 214
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 213 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
43com12 29 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  biimprcd  217  nfsb4t  2129  elsnc2g  3802  opth1  4394  euotd  4417  tz7.2  4526  ordtri1  4574  reusv2lem2  4684  reusv3  4690  alxfr  4695  reuhypd  4709  oneqmin  4744  nlimsucg  4781  onzsl  4785  tfinds  4798  xpsspw  4945  funcnvuni  5477  fvmptdv2  5777  foco2  5848  fsn  5865  fconst2g  5905  fnpr  5909  fnprOLD  5910  funfvima  5932  soisoi  6007  isores3  6014  ovmpt2dv2  6166  f1opw2  6257  suppssfv  6260  suppssov1  6261  brtpos  6447  sorpssun  6488  sorpssin  6489  opiota  6494  eusvobj2  6541  riotaclbg  6548  seqomlem1  6666  seqomlem2  6667  omordi  6768  omord  6770  omwordi  6773  oeeui  6804  nnmordi  6833  nnmord  6834  nnmwordi  6837  nnawordex  6839  nnaordex  6840  nneob  6854  omsmolem  6855  qsss  6924  eroveu  6958  th3qlem1  6969  mapsncnv  7019  elixpsn  7060  ixpsnf1o  7061  boxcutc  7064  pw2f1olem  7171  2pwne  7222  mapxpen  7232  mapunen  7235  php  7250  unxpdomlem2  7273  isfiniteg  7326  fofinf1o  7346  f1opwfi  7368  elfiun  7393  oieu  7464  brwdom2  7497  wdomtr  7499  ixpiunwdom  7515  suc11reg  7530  inf3lemd  7538  cantnfvalf  7576  cantnflt  7583  cantnfp1lem3  7592  cantnflem2  7602  en3lplem1  7626  r1tr  7658  dfac8alem  7866  wdomnumr  7901  isinfcard  7929  aceq3lem  7957  dfac5lem4  7963  dfac5  7965  dfac2  7967  coftr  8109  fin23lem28  8176  fin23lem29  8177  fin1a2lem11  8246  fin1a2lem12  8247  fin1a2lem13  8248  hsmexlem9  8261  axdclem  8355  pwcfsdom  8414  gchdomtri  8460  fpwwe2  8474  gchhar  8502  gchpwdom  8505  addnidpi  8734  nqereu  8762  genpv  8832  genpdm  8835  distrlem5pr  8860  mulid1  9044  ltne  9126  mul02  9200  cnegex  9203  mul0or  9618  sup2  9920  supmul1  9929  supmul  9932  creur  9950  creui  9951  cju  9952  nnsub  9994  un0addcl  10209  un0mulcl  10210  nn0sub  10226  elz2  10254  zaddcl  10273  suprzcl2  10522  qmulz  10533  qre  10535  qnegcl  10547  xrmax1  10719  xrmin2  10722  max1ALT  10730  xlesubadd  10798  xmulass  10822  xlemul1a  10823  xrsupexmnf  10839  xrinfmexpnf  10840  xrub  10846  iccid  10917  fzsn  11050  fzsuc2  11060  fz1sbc  11079  elfzp12  11081  fzm1  11082  seqid3  11322  bcval5  11564  bcpasc  11567  hashbnd  11579  hashnnn0genn0  11582  hashprg  11621  hashfzo  11649  cats1un  11745  shftlem  11838  replim  11876  absmod0  12063  absz  12071  rlimdm  12300  summolem2  12465  summo  12466  zsum  12467  fsum  12469  fsummulc2  12522  fsumconst  12528  fsum00  12532  incexclem  12571  isumsplit  12575  infcvgaux1i  12591  ruclem2  12786  fzo0dvdseq  12857  bitsf1ocnv  12911  sadcaddlem  12924  smueqlem  12957  gcdabs1  12989  bezoutlem1  12993  bezoutlem3  12995  bezoutlem4  12996  dvdsgcd  12998  dvdsmulgcd  13009  dvdsprime  13047  coprm  13055  isprm5  13067  prmdvdsexpr  13071  rpexp  13075  phibndlem  13114  dfphi2  13118  odzdvds  13136  pythagtriplem1  13145  iserodd  13164  pceulem  13174  pcqmul  13182  pcqcl  13185  pcxcl  13189  pcneg  13202  pcabs  13203  pcgcd1  13205  pcz  13209  pcprmpw2  13210  pcprmpw  13211  pcaddlem  13212  pcadd  13213  pcmpt  13216  pockthg  13229  prmreclem5  13243  4sqlem4  13275  mul4sq  13277  vdwapun  13297  vdwlem2  13305  vdwlem6  13309  vdwlem8  13311  vdwlem13  13316  0ram  13343  ram0  13345  ramcl  13352  wunress  13483  firest  13615  xpscfv  13742  isssc  13975  pospo  14385  latnlej  14452  gsumval2a  14737  mulgnn0p1  14856  mulgnn0ass  14874  gicsubgen  15020  mndodcongi  15136  oddvdsnn0  15137  odnncl  15138  oddvds  15140  odeq  15143  odeq1  15151  pgpfi2  15195  sylow2a  15208  sylow2blem3  15211  sylow3lem6  15221  lsmelvalm  15240  lsmsubm  15242  lsmsubg  15243  lsmmod  15262  lsmdisj2  15269  efgmnvl  15301  efgtlen  15313  efgs1b  15323  efgrelexlemb  15337  efgredeu  15339  efgcpbllemb  15342  frgpuptinv  15358  frgpup3lem  15364  divsabl  15435  frgpnabllem1  15439  cyggeninv  15448  cyggenod  15449  cygabl  15455  gsumval3eu  15468  dprdssv  15529  dprdfeq0  15535  dprdsubg  15537  dprddisj2  15552  ablfacrp  15579  pgpfac1lem3  15590  pgpfaclem2  15595  dvreq1  15753  irredn1  15766  drngmul0or  15811  isabvd  15863  abvdom  15881  issrngd  15904  lss1d  15994  lspsneq0  16043  lbspss  16109  lsmcl  16110  lvecvs0or  16135  lspindpi  16159  lidl1el  16244  lpiss  16276  lidldvgen  16281  nzrunit  16292  rrgeq0  16305  domneq0  16312  mplsubrglem  16457  mplmonmul  16482  coe1tmmul2  16623  coe1tmmul  16624  qsssubdrg  16713  zlpirlem1  16723  znfld  16796  znunit  16799  znrrg  16801  cygznlem3  16805  frgpcyg  16809  ipeq0  16824  cssincl  16870  lsmcss  16874  obselocv  16910  istopon  16945  eltg3  16982  tgidm  17000  clsval2  17069  opncldf1  17103  restbas  17176  tgrest  17177  restcld  17190  restcldr  17192  restcls  17199  restntr  17200  ordtbas2  17209  ordtbas  17210  ordtrest2lem  17221  ordtrest2  17222  pnfnei  17238  mnfnei  17239  tgcn  17270  cnconst  17302  cnindis  17310  lmss  17316  ordtt1  17397  discmp  17415  1stcrest  17469  2ndcdisj  17472  cldllycmp  17511  txbas  17552  ptpjpre1  17556  ptuni2  17561  ptbasin  17562  ptbasfi  17566  ptopn2  17569  txbasval  17591  ptpjopn  17597  ptclsg  17600  dfac14lem  17602  xkoccn  17604  ptcnp  17607  upxp  17608  ptrescn  17624  txkgen  17637  xkoptsub  17639  xkopt  17640  xkoco1cn  17642  xkoco2cn  17643  xkococn  17645  xkoinjcn  17672  ordthmeolem  17786  ptuncnv  17792  nrmhaus  17811  fbssint  17823  fbfinnfr  17826  fbasrn  17869  isufil2  17893  filufint  17905  rnelfm  17938  fmfnfmlem2  17940  fmfnfmlem3  17941  fmfnfmlem4  17942  fmfnfm  17943  flimtopon  17955  flimclslem  17969  fclstopon  17997  fclscf  18010  flimfnfcls  18013  alexsublem  18028  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem2  18037  tmdgsum2  18079  symgtgp  18084  cldsubg  18093  divstgplem  18103  tgptsmscld  18133  tsmsxplem1  18135  imasdsf1olem  18356  blssps  18407  blss  18408  stdbdxmet  18498  methaus  18503  metrest  18507  nrginvrcn  18680  nmoeq0  18723  blssioo  18779  xrtgioo  18790  xrsxmet  18793  reconnlem1  18810  reconnlem2  18811  xrge0tsms  18818  elcncf1di  18878  iccpnfcnv  18922  evth  18937  lebnumlem1  18939  lebnumlem2  18940  lebnumlem3  18941  nmoleub3  19080  minveclem3b  19282  ivthlem2  19302  ivthlem3  19303  elovolm  19324  ovolmge0  19326  ovoliun  19354  ovolicc2lem3  19368  ovolicc2  19371  voliunlem3  19399  dyaddisj  19441  dyadmax  19443  opnmblALT  19448  ismbfd  19485  ismbf2d  19486  mbfimaopnlem  19500  mbfimaopn2  19502  i1fmullem  19539  i1fres  19550  itg1climres  19559  mbfi1fseqlem4  19563  itg2lcl  19572  itgsplitioo  19682  ellimc2  19717  rolle  19827  dvlip  19830  dvge0  19843  dvne0  19848  lhop1lem  19850  pf1ind  19928  tdeglem4  19936  degltlem1  19948  deg1nn0clb  19966  deg1lt0  19967  dvdsq1p  20036  ply1rem  20039  fta1g  20043  elply2  20068  plyf  20070  ne0p  20079  plyeq0lem  20082  plypf1  20084  0dgrb  20118  coe1termlem  20129  dgrcolem2  20145  plymul0or  20151  plyrem  20175  fta1  20178  quotcan  20179  aalioulem3  20204  eff1olem  20403  lognegb  20437  eflogeq  20449  argregt0  20458  argrege0  20459  tanarg  20467  cxpexp  20512  cxpeq0  20522  mulcxp  20529  cxpeq  20594  atans2  20724  scvxcvx  20777  isppw2  20851  vmappw  20852  vmacl  20854  efvmacl  20856  isnsqf  20871  mumullem2  20916  sqff1o  20918  dvdsppwf1o  20924  ppiublem1  20939  vmalelog  20942  chtublem  20948  fsumvma  20950  perfectlem2  20967  perfect  20968  bposlem1  21021  lgsmod  21058  lgsne0  21070  lgsdirnn0  21076  lgsqr  21083  lgsdchr  21085  lgseisenlem2  21087  lgsquadlem1  21091  lgsquadlem2  21092  2sqlem2  21101  mul2sq  21102  2sqlem7  21107  dchrisum0fno1  21158  pntrsumbnd2  21214  ostthlem1  21274  ostth2lem2  21281  ostth3  21285  ostth  21286  usgraexmpl  21373  nbgraf1olem1  21404  nbgraf1olem3  21406  nbgraf1olem5  21408  nb3graprlem2  21414  cusgrasize2inds  21439  vdgr1a  21630  vdusgra0nedg  21632  usgravd0nedg  21636  eupap1  21651  ismndo2  21886  ghgrplem1  21907  rngosn4  21968  nvmul0or  22086  ipasslem5  22289  ipasslem11  22294  hvmul0or  22480  his6  22554  hhssnv  22717  ocsh  22738  ocin  22751  shsidmi  22839  chnlen0  22899  h1de2bi  23009  h1de2ctlem  23010  h1de2ci  23011  spansni  23012  3oalem1  23117  nmcexi  23482  atcveq0  23804  chcv1  23811  cdjreui  23888  cdj3lem2b  23893  xrge0tsmsd  24176  xrge0iifcnv  24272  esumc  24399  esumpcvgval  24421  ballotlemfc0  24703  ballotlemfcc  24704  dmgmaddn0  24760  subfacp1lem4  24822  subfacp1lem5  24823  erdszelem8  24837  sconpi1  24879  cvmsss2  24914  cvmlift2lem12  24954  sinccvglem  25062  untsucf  25112  prodmolem2  25214  prodmo  25215  zprod  25216  fprod  25220  prodsn  25239  fprodconst  25255  dfpo2  25326  dfrdg2  25366  trpred0  25453  wfrlem14  25483  wfrlem15  25484  frrlem4  25498  colinearalg  25753  axpasch  25784  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim  25804  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  colineardim1  25899  btwnconn1lem14  25938  segleantisym  25953  colinbtwnle  25956  outsidele  25970  lineunray  25985  linethru  25991  supaddc  26137  supadd  26138  itg2addnclem3  26157  elicc3  26210  opnregcld  26223  cldregopn  26224  fnejoin2  26288  unirep  26304  sdclem2  26336  ssbnd  26387  prdsbnd  26392  cntotbnd  26395  heibor1lem  26408  rrnequiv  26434  grpoeqdivid  26446  isdrngo3  26465  crngohomfo  26506  0idl  26525  1idl  26526  divrngidl  26528  smprngopr  26552  prnc  26567  ispridlc  26570  ralxpmap  26632  elrfi  26638  mrefg2  26651  eldiophb  26705  eldioph2b  26711  diophin  26721  diophun  26722  rexzrexnn0  26754  eldioph4b  26762  diophren  26764  rencldnfilem  26771  pellexlem6  26787  jm2.19  26954  rmydioph  26975  expdiophlem1  26982  expdioph  26984  dsmmacl  27075  dsmmlss  27078  lnr2i  27188  lpirlnr  27189  hbtlem2  27196  hbtlem4  27198  hbtlem6  27201  dgrsub2  27207  dgraa0p  27222  rngunsnply  27246  psgnunilem1  27284  psgnunilem2  27286  psgnghm  27305  hashgcdlem  27384  pm14.24  27500  addrcom  27547  afveu  27884  dfafn5b  27892  rlimdmafv  27908  swrdccat3b  28031  vdn0frgrav2  28128  vdgn0frgrav2  28129  bnj145  28800  nfsb4twAUX7  29280  nfsb4tOLD7  29429  nfsb4tw2AUXOLD7  29430  lshpdisj  29470  lsateln0  29478  lsatcveq0  29515  opnlen0  29671  glb0N  29676  cmtbr4N  29738  cvrnbtwn2  29758  cvrnbtwn4  29762  atcvreq0  29797  cvlatexch1  29819  exatleN  29886  atlelt  29920  ps-2  29960  llnn0  29998  lplnn0N  30029  islpln2a  30030  lvoln0N  30073  islvol2aN  30074  4at  30095  dalemcea  30142  dalem3  30146  pmapglb2N  30253  pmapglb2xN  30254  cdlema1N  30273  cdlemb  30276  paddasslem17  30318  llnexchb2lem  30350  llnexchb2  30351  lhpat3  30528  ltrnid  30617  trlne  30667  cdlemc4  30676  cdleme11h  30748  cdlemednuN  30782  cdlemg1a  31052  tendoeq2  31256  tendoid0  31307  dva1dim  31467  dib1dim  31648  dihlatat  31820  dochkrshp4  31872  dochkr1  31961  lclkrlem2e  31994  lcfrlem16  32041  lcfrlem28  32053  mapd0  32148  hdmap14lem13  32366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator