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

Theorem syl5ibrcom 215
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 214 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
43com12 30 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  biimprcd  218  nfsb4tOLD  2130  elsnc2g  3844  opth1  4436  euotd  4459  tz7.2  4568  ordtri1  4616  reusv2lem2  4727  reusv3  4733  alxfr  4738  reuhypd  4752  oneqmin  4787  nlimsucg  4824  onzsl  4828  tfinds  4841  xpsspw  4988  funcnvuni  5520  fvmptdv2  5820  foco2  5891  fsn  5908  fconst2g  5948  fnpr  5952  fnprOLD  5953  funfvima  5975  soisoi  6050  isores3  6057  ovmpt2dv2  6209  f1opw2  6300  suppssfv  6303  suppssov1  6304  brtpos  6490  sorpssun  6531  sorpssin  6532  opiota  6537  eusvobj2  6584  riotaclbg  6591  seqomlem1  6709  seqomlem2  6710  omordi  6811  omord  6813  omwordi  6816  oeeui  6847  nnmordi  6876  nnmord  6877  nnmwordi  6880  nnawordex  6882  nnaordex  6883  nneob  6897  omsmolem  6898  qsss  6967  eroveu  7001  th3qlem1  7012  mapsncnv  7062  elixpsn  7103  ixpsnf1o  7104  boxcutc  7107  pw2f1olem  7214  2pwne  7265  mapxpen  7275  mapunen  7278  php  7293  unxpdomlem2  7316  isfiniteg  7369  fofinf1o  7389  f1opwfi  7412  elfiun  7437  oieu  7510  brwdom2  7543  wdomtr  7545  ixpiunwdom  7561  suc11reg  7576  inf3lemd  7584  cantnfvalf  7622  cantnflt  7629  cantnfp1lem3  7638  cantnflem2  7648  en3lplem1  7672  r1tr  7704  dfac8alem  7912  wdomnumr  7947  isinfcard  7975  aceq3lem  8003  dfac5lem4  8009  dfac5  8011  dfac2  8013  coftr  8155  fin23lem28  8222  fin23lem29  8223  fin1a2lem11  8292  fin1a2lem12  8293  fin1a2lem13  8294  hsmexlem9  8307  axdclem  8401  pwcfsdom  8460  gchdomtri  8506  fpwwe2  8520  gchhar  8548  gchpwdom  8551  addnidpi  8780  nqereu  8808  genpv  8878  genpdm  8881  distrlem5pr  8906  mulid1  9090  ltne  9172  mul02  9246  cnegex  9249  mul0or  9664  sup2  9966  supmul1  9975  supmul  9978  creur  9996  creui  9997  cju  9998  nnsub  10040  un0addcl  10255  un0mulcl  10256  nn0sub  10272  elz2  10300  zaddcl  10319  suprzcl2  10568  qmulz  10579  qre  10581  qnegcl  10593  xrmax1  10765  xrmin2  10768  max1ALT  10776  xlesubadd  10844  xmulass  10868  xlemul1a  10869  xrsupexmnf  10885  xrinfmexpnf  10886  xrub  10892  iccid  10963  fzsn  11096  fzsuc2  11106  fz1sbc  11126  elfzp12  11128  fzm1  11129  seqid3  11369  bcval5  11611  bcpasc  11614  hashbnd  11626  hashnnn0genn0  11629  hashprg  11668  hashfzo  11696  cats1un  11792  shftlem  11885  replim  11923  absmod0  12110  absz  12118  rlimdm  12347  summolem2  12512  summo  12513  zsum  12514  fsum  12516  fsummulc2  12569  fsumconst  12575  fsum00  12579  incexclem  12618  isumsplit  12622  infcvgaux1i  12638  ruclem2  12833  fzo0dvdseq  12904  bitsf1ocnv  12958  sadcaddlem  12971  smueqlem  13004  gcdabs1  13036  bezoutlem1  13040  bezoutlem3  13042  bezoutlem4  13043  dvdsgcd  13045  dvdsmulgcd  13056  dvdsprime  13094  coprm  13102  isprm5  13114  prmdvdsexpr  13118  rpexp  13122  phibndlem  13161  dfphi2  13165  odzdvds  13183  pythagtriplem1  13192  iserodd  13211  pceulem  13221  pcqmul  13229  pcqcl  13232  pcxcl  13236  pcneg  13249  pcabs  13250  pcgcd1  13252  pcz  13256  pcprmpw2  13257  pcprmpw  13258  pcaddlem  13259  pcadd  13260  pcmpt  13263  pockthg  13276  prmreclem5  13290  4sqlem4  13322  mul4sq  13324  vdwapun  13344  vdwlem2  13352  vdwlem6  13356  vdwlem8  13358  vdwlem13  13363  0ram  13390  ram0  13392  ramcl  13399  wunress  13530  firest  13662  xpscfv  13789  isssc  14022  pospo  14432  latnlej  14499  gsumval2a  14784  mulgnn0p1  14903  mulgnn0ass  14921  gicsubgen  15067  mndodcongi  15183  oddvdsnn0  15184  odnncl  15185  oddvds  15187  odeq  15190  odeq1  15198  pgpfi2  15242  sylow2a  15255  sylow2blem3  15258  sylow3lem6  15268  lsmelvalm  15287  lsmsubm  15289  lsmsubg  15290  lsmmod  15309  lsmdisj2  15316  efgmnvl  15348  efgtlen  15360  efgs1b  15370  efgrelexlemb  15384  efgredeu  15386  efgcpbllemb  15389  frgpuptinv  15405  frgpup3lem  15411  divsabl  15482  frgpnabllem1  15486  cyggeninv  15495  cyggenod  15496  cygabl  15502  gsumval3eu  15515  dprdssv  15576  dprdfeq0  15582  dprdsubg  15584  dprddisj2  15599  ablfacrp  15626  pgpfac1lem3  15637  pgpfaclem2  15642  dvreq1  15800  irredn1  15813  drngmul0or  15858  isabvd  15910  abvdom  15928  issrngd  15951  lss1d  16041  lspsneq0  16090  lbspss  16156  lsmcl  16157  lvecvs0or  16182  lspindpi  16206  lidl1el  16291  lpiss  16323  lidldvgen  16328  nzrunit  16339  rrgeq0  16352  domneq0  16359  mplsubrglem  16504  mplmonmul  16529  coe1tmmul2  16670  coe1tmmul  16671  qsssubdrg  16760  zlpirlem1  16770  znfld  16843  znunit  16846  znrrg  16848  cygznlem3  16852  frgpcyg  16856  ipeq0  16871  cssincl  16917  lsmcss  16921  obselocv  16957  istopon  16992  eltg3  17029  tgidm  17047  clsval2  17116  opncldf1  17150  restbas  17224  tgrest  17225  restcld  17238  restcldr  17240  restcls  17247  restntr  17248  ordtbas2  17257  ordtbas  17258  ordtrest2lem  17269  ordtrest2  17270  pnfnei  17286  mnfnei  17287  tgcn  17318  cnconst  17350  cnindis  17358  lmss  17364  ordtt1  17445  discmp  17463  1stcrest  17518  2ndcdisj  17521  cldllycmp  17560  txbas  17601  ptpjpre1  17605  ptuni2  17610  ptbasin  17611  ptbasfi  17615  ptopn2  17618  txbasval  17640  ptpjopn  17646  ptclsg  17649  dfac14lem  17651  xkoccn  17653  ptcnp  17656  upxp  17657  ptrescn  17673  txkgen  17686  xkoptsub  17688  xkopt  17689  xkoco1cn  17691  xkoco2cn  17692  xkococn  17694  xkoinjcn  17721  ordthmeolem  17835  ptuncnv  17841  nrmhaus  17860  fbssint  17872  fbfinnfr  17875  fbasrn  17918  isufil2  17942  filufint  17954  rnelfm  17987  fmfnfmlem2  17989  fmfnfmlem3  17990  fmfnfmlem4  17991  fmfnfm  17992  flimtopon  18004  flimclslem  18018  fclstopon  18046  fclscf  18059  flimfnfcls  18062  alexsublem  18077  alexsubALTlem3  18082  alexsubALTlem4  18083  ptcmplem2  18086  tmdgsum2  18128  symgtgp  18133  cldsubg  18142  divstgplem  18152  tgptsmscld  18182  tsmsxplem1  18184  imasdsf1olem  18405  blssps  18456  blss  18457  stdbdxmet  18547  methaus  18552  metrest  18556  nrginvrcn  18729  nmoeq0  18772  blssioo  18828  xrtgioo  18839  xrsxmet  18842  reconnlem1  18859  reconnlem2  18860  xrge0tsms  18867  elcncf1di  18927  iccpnfcnv  18971  evth  18986  lebnumlem1  18988  lebnumlem2  18989  lebnumlem3  18990  nmoleub3  19129  minveclem3b  19331  ivthlem2  19351  ivthlem3  19352  elovolm  19373  ovolmge0  19375  ovoliun  19403  ovolicc2lem3  19417  ovolicc2  19420  voliunlem3  19448  dyaddisj  19490  dyadmax  19492  opnmblALT  19497  ismbfd  19534  ismbf2d  19535  mbfimaopnlem  19549  mbfimaopn2  19551  i1fmullem  19588  i1fres  19599  itg1climres  19608  mbfi1fseqlem4  19612  itg2lcl  19621  itgsplitioo  19731  ellimc2  19766  rolle  19876  dvlip  19879  dvge0  19892  dvne0  19897  lhop1lem  19899  pf1ind  19977  tdeglem4  19985  degltlem1  19997  deg1nn0clb  20015  deg1lt0  20016  dvdsq1p  20085  ply1rem  20088  fta1g  20092  elply2  20117  plyf  20119  ne0p  20128  plyeq0lem  20131  plypf1  20133  0dgrb  20167  coe1termlem  20178  dgrcolem2  20194  plymul0or  20200  plyrem  20224  fta1  20227  quotcan  20228  aalioulem3  20253  eff1olem  20452  lognegb  20486  eflogeq  20498  argregt0  20507  argrege0  20508  tanarg  20516  cxpexp  20561  cxpeq0  20571  mulcxp  20578  cxpeq  20643  atans2  20773  scvxcvx  20826  isppw2  20900  vmappw  20901  vmacl  20903  efvmacl  20905  isnsqf  20920  mumullem2  20965  sqff1o  20967  dvdsppwf1o  20973  ppiublem1  20988  vmalelog  20991  chtublem  20997  fsumvma  20999  perfectlem2  21016  perfect  21017  bposlem1  21070  lgsmod  21107  lgsne0  21119  lgsdirnn0  21125  lgsqr  21132  lgsdchr  21134  lgseisenlem2  21136  lgsquadlem1  21140  lgsquadlem2  21141  2sqlem2  21150  mul2sq  21151  2sqlem7  21156  dchrisum0fno1  21207  pntrsumbnd2  21263  ostthlem1  21323  ostth2lem2  21330  ostth3  21334  ostth  21335  usgraexmpl  21422  nbgraf1olem1  21453  nbgraf1olem3  21455  nbgraf1olem5  21457  nb3graprlem2  21463  cusgrasize2inds  21488  vdgr1a  21679  vdusgra0nedg  21681  usgravd0nedg  21685  eupap1  21700  ismndo2  21935  ghgrplem1  21956  rngosn4  22017  nvmul0or  22135  ipasslem5  22338  ipasslem11  22343  hvmul0or  22529  his6  22603  hhssnv  22766  ocsh  22787  ocin  22800  shsidmi  22888  chnlen0  22948  h1de2bi  23058  h1de2ctlem  23059  h1de2ci  23060  spansni  23061  3oalem1  23166  nmcexi  23531  atcveq0  23853  chcv1  23860  cdjreui  23937  cdj3lem2b  23942  xrge0tsmsd  24225  xrge0iifcnv  24321  esumc  24448  esumpcvgval  24470  ballotlemfc0  24752  ballotlemfcc  24753  dmgmaddn0  24809  subfacp1lem4  24871  subfacp1lem5  24872  erdszelem8  24886  sconpi1  24928  cvmsss2  24963  cvmlift2lem12  25003  sinccvglem  25111  untsucf  25161  prodmolem2  25263  prodmo  25264  zprod  25265  fprod  25269  prodsn  25288  fprodconst  25304  dfpo2  25380  dfrdg2  25425  trpred0  25516  wfrlem10  25549  wfrlem14  25553  wfrlem15  25554  frrlem4  25587  colinearalg  25851  axpasch  25882  axlowdimlem16  25898  axlowdimlem17  25899  axlowdim  25902  axcontlem2  25906  axcontlem4  25908  axcontlem7  25911  colineardim1  25997  btwnconn1lem14  26036  segleantisym  26051  colinbtwnle  26054  outsidele  26068  lineunray  26083  linethru  26089  supaddc  26239  supadd  26240  itg2addnclem3  26260  ftc1anclem6  26287  elicc3  26322  opnregcld  26335  cldregopn  26336  fnejoin2  26400  unirep  26416  sdclem2  26448  ssbnd  26499  prdsbnd  26504  cntotbnd  26507  heibor1lem  26520  rrnequiv  26546  grpoeqdivid  26558  isdrngo3  26577  crngohomfo  26618  0idl  26637  1idl  26638  divrngidl  26640  smprngopr  26664  prnc  26679  ispridlc  26682  ralxpmap  26744  elrfi  26750  mrefg2  26763  eldiophb  26817  eldioph2b  26823  diophin  26833  diophun  26834  rexzrexnn0  26866  eldioph4b  26874  diophren  26876  rencldnfilem  26883  pellexlem6  26899  jm2.19  27066  rmydioph  27087  expdiophlem1  27094  expdioph  27096  dsmmacl  27186  dsmmlss  27189  lnr2i  27299  lpirlnr  27300  hbtlem2  27307  hbtlem4  27309  hbtlem6  27312  dgrsub2  27318  dgraa0p  27333  rngunsnply  27357  psgnunilem1  27395  psgnunilem2  27397  psgnghm  27416  hashgcdlem  27495  pm14.24  27611  addrcom  27658  afveu  27995  dfafn5b  28003  rlimdmafv  28019  cshwsiun  28308  wlklenfislenpm1  28325  wlklniswwlkn2  28370  0eusgraiff0rgra  28438  vdn0frgrav2  28476  vdgn0frgrav2  28477  bnj145  29156  nfsb4twAUX7  29638  nfsb4tOLD7  29807  nfsb4tw2AUXOLD7  29808  lshpdisj  29847  lsateln0  29855  lsatcveq0  29892  opnlen0  30048  glb0N  30053  cmtbr4N  30115  cvrnbtwn2  30135  cvrnbtwn4  30139  atcvreq0  30174  cvlatexch1  30196  exatleN  30263  atlelt  30297  ps-2  30337  llnn0  30375  lplnn0N  30406  islpln2a  30407  lvoln0N  30450  islvol2aN  30451  4at  30472  dalemcea  30519  dalem3  30523  pmapglb2N  30630  pmapglb2xN  30631  cdlema1N  30650  cdlemb  30653  paddasslem17  30695  llnexchb2lem  30727  llnexchb2  30728  lhpat3  30905  ltrnid  30994  trlne  31044  cdlemc4  31053  cdleme11h  31125  cdlemednuN  31159  cdlemg1a  31429  tendoeq2  31633  tendoid0  31684  dva1dim  31844  dib1dim  32025  dihlatat  32197  dochkrshp4  32249  dochkr1  32338  lclkrlem2e  32371  lcfrlem16  32418  lcfrlem28  32430  mapd0  32525  hdmap14lem13  32743
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 179
  Copyright terms: Public domain W3C validator