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

Theorem syl5ibrcom 213
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 212 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
43com12 27 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  biimprcd  216  nfsb4t  2020  elsnc2g  3668  opth1  4244  euotd  4267  tz7.2  4377  ordtri1  4425  reusv2lem2  4536  reusv3  4542  alxfr  4547  reuhypd  4561  oneqmin  4596  nlimsucg  4633  onzsl  4637  tfinds  4650  xpsspw  4797  funcnvuni  5317  fvmptdv2  5613  foco2  5680  fsn  5696  fconst2g  5728  funfvima  5753  soisoi  5825  isores3  5832  ovmpt2dv2  5981  f1opw2  6071  suppssfv  6074  suppssov1  6075  brtpos  6243  sorpssun  6284  sorpssin  6285  opiota  6290  eusvobj2  6337  riotaclbg  6344  seqomlem1  6462  seqomlem2  6463  omordi  6564  omord  6566  omwordi  6569  oeeui  6600  nnmordi  6629  nnmord  6630  nnmwordi  6633  nnawordex  6635  nnaordex  6636  nneob  6650  omsmolem  6651  qsss  6720  eroveu  6753  th3qlem1  6764  mapsncnv  6814  elixpsn  6855  ixpsnf1o  6856  boxcutc  6859  pw2f1olem  6966  2pwne  7017  mapxpen  7027  mapunen  7030  php  7045  unxpdomlem2  7068  isfiniteg  7117  fofinf1o  7137  f1opwfi  7159  elfiun  7183  oieu  7254  brwdom2  7287  wdomtr  7289  ixpiunwdom  7305  suc11reg  7320  inf3lemd  7328  cantnfvalf  7366  cantnflt  7373  cantnfp1lem3  7382  cantnflem2  7392  en3lplem1  7416  r1tr  7448  dfac8alem  7656  wdomnumr  7691  isinfcard  7719  aceq3lem  7747  dfac5lem4  7753  dfac5  7755  dfac2  7757  coftr  7899  fin23lem28  7966  fin23lem29  7967  fin1a2lem11  8036  fin1a2lem12  8037  fin1a2lem13  8038  hsmexlem9  8051  axdclem  8146  pwcfsdom  8205  gchdomtri  8251  fpwwe2  8265  gchhar  8293  gchpwdom  8296  addnidpi  8525  nqereu  8553  genpv  8623  genpdm  8626  distrlem5pr  8651  mulid1  8835  ltne  8917  mul02  8990  cnegex  8993  mul0or  9408  sup2  9710  supmul1  9719  supmul  9722  creur  9740  creui  9741  cju  9742  nnsub  9784  un0addcl  9997  un0mulcl  9998  nn0sub  10014  elz2  10040  zaddcl  10059  suprzcl2  10308  qmulz  10319  qre  10321  qnegcl  10333  xrmax1  10504  xrmin2  10507  max1ALT  10515  xlesubadd  10583  xmulass  10607  xlemul1a  10608  xrsupexmnf  10623  xrinfmexpnf  10624  xrub  10630  iccid  10701  fzsn  10833  fzsuc2  10842  fz1sbc  10859  elfzp12  10861  fzm1  10862  seqid3  11090  bcval5  11330  bcpasc  11333  hashbnd  11343  hashprg  11368  hashfzo  11383  cats1un  11476  shftlem  11563  replim  11601  absmod0  11788  absz  11796  rlimdm  12025  summolem2  12189  summo  12190  zsum  12191  fsum  12193  fsummulc2  12246  fsumconst  12252  fsum00  12256  incexclem  12295  isumsplit  12299  infcvgaux1i  12315  ruclem2  12510  fzo0dvdseq  12581  bitsf1ocnv  12635  sadcaddlem  12648  smueqlem  12681  gcdabs1  12713  bezoutlem1  12717  bezoutlem3  12719  bezoutlem4  12720  dvdsgcd  12722  dvdsmulgcd  12733  dvdsprime  12771  coprm  12779  isprm5  12791  prmdvdsexpr  12795  rpexp  12799  phibndlem  12838  dfphi2  12842  odzdvds  12860  pythagtriplem1  12869  iserodd  12888  pceulem  12898  pcqmul  12906  pcqcl  12909  pcxcl  12913  pcneg  12926  pcabs  12927  pcgcd1  12929  pcz  12933  pcprmpw2  12934  pcprmpw  12935  pcaddlem  12936  pcadd  12937  pcmpt  12940  pockthg  12953  prmreclem5  12967  4sqlem4  12999  mul4sq  13001  vdwapun  13021  vdwlem2  13029  vdwlem6  13033  vdwlem8  13035  vdwlem13  13040  0ram  13067  ram0  13069  ramcl  13076  wunress  13207  firest  13337  xpscfv  13464  isssc  13697  pospo  14107  latnlej  14174  gsumval2a  14459  mulgnn0p1  14578  mulgnn0ass  14596  gicsubgen  14742  mndodcongi  14858  oddvdsnn0  14859  odnncl  14860  oddvds  14862  odeq  14865  odeq1  14873  pgpfi2  14917  sylow2a  14930  sylow2blem3  14933  sylow3lem6  14943  lsmelvalm  14962  lsmsubm  14964  lsmsubg  14965  lsmmod  14984  lsmdisj2  14991  efgmnvl  15023  efgtlen  15035  efgs1b  15045  efgrelexlemb  15059  efgredeu  15061  efgcpbllemb  15064  frgpuptinv  15080  frgpup3lem  15086  divsabl  15157  frgpnabllem1  15161  cyggeninv  15170  cyggenod  15171  cygabl  15177  gsumval3eu  15190  dprdssv  15251  dprdfeq0  15257  dprdsubg  15259  dprddisj2  15274  ablfacrp  15301  pgpfac1lem3  15312  pgpfaclem2  15317  dvreq1  15475  irredn1  15488  drngmul0or  15533  isabvd  15585  abvdom  15603  issrngd  15626  lss1d  15720  lspsneq0  15769  lbspss  15835  lsmcl  15836  lvecvs0or  15861  lspindpi  15885  lidl1el  15970  lpiss  16002  lidldvgen  16007  nzrunit  16018  rrgeq0  16031  domneq0  16038  mplsubrglem  16183  mplmonmul  16208  coe1tmmul2  16352  coe1tmmul  16353  qsssubdrg  16431  zlpirlem1  16441  znfld  16514  znunit  16517  znrrg  16519  cygznlem3  16523  frgpcyg  16527  ipeq0  16542  cssincl  16588  lsmcss  16592  obselocv  16628  istopon  16663  eltg3  16700  tgidm  16718  clsval2  16787  opncldf1  16821  restbas  16889  tgrest  16890  restcld  16903  restcldr  16905  restcls  16911  restntr  16912  ordtbas2  16921  ordtbas  16922  ordtrest2lem  16933  ordtrest2  16934  pnfnei  16950  mnfnei  16951  tgcn  16982  cnconst  17012  cnindis  17020  lmss  17026  ordtt1  17107  discmp  17125  1stcrest  17179  2ndcdisj  17182  cldllycmp  17221  txbas  17262  ptpjpre1  17266  ptuni2  17271  ptbasin  17272  ptbasfi  17276  ptopn2  17279  txbasval  17301  ptpjopn  17306  ptclsg  17309  dfac14lem  17311  xkoccn  17313  ptcnp  17316  upxp  17317  ptrescn  17333  txkgen  17346  xkoptsub  17348  xkopt  17349  xkoco1cn  17351  xkoco2cn  17352  xkococn  17354  xkoinjcn  17381  ordthmeolem  17492  ptuncnv  17498  nrmhaus  17517  fbssint  17533  fbfinnfr  17536  fbasrn  17579  isufil2  17603  filufint  17615  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem3  17651  fmfnfmlem4  17652  fmfnfm  17653  flimtopon  17665  flimclslem  17679  fclstopon  17707  fclscf  17720  flimfnfcls  17723  alexsublem  17738  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem2  17747  tmdgsum2  17779  symgtgp  17784  cldsubg  17793  divstgplem  17803  tgptsmscld  17833  tsmsxplem1  17835  imasdsf1olem  17937  blss  17972  stdbdxmet  18061  methaus  18066  metrest  18070  nrginvrcn  18202  nmoeq0  18245  blssioo  18301  xrtgioo  18312  xrsxmet  18315  reconnlem1  18331  reconnlem2  18332  xrge0tsms  18339  elcncf1di  18399  iccpnfcnv  18442  evth  18457  lebnumlem1  18459  lebnumlem2  18460  lebnumlem3  18461  nmoleub3  18600  minveclem3b  18792  ivthlem2  18812  ivthlem3  18813  elovolm  18834  ovolmge0  18836  ovoliun  18864  ovolicc2lem3  18878  ovolicc2  18881  voliunlem3  18909  dyaddisj  18951  dyadmax  18953  opnmblALT  18958  ismbfd  18995  ismbf2d  18996  mbfimaopnlem  19010  mbfimaopn2  19012  i1fmullem  19049  i1fres  19060  itg1climres  19069  mbfi1fseqlem4  19073  itg2lcl  19082  itgsplitioo  19192  ellimc2  19227  rolle  19337  dvlip  19340  dvge0  19353  dvne0  19358  lhop1lem  19360  pf1ind  19438  tdeglem4  19446  degltlem1  19458  deg1nn0clb  19476  deg1lt0  19477  dvdsq1p  19546  ply1rem  19549  fta1g  19553  elply2  19578  plyf  19580  ne0p  19589  plyeq0lem  19592  plypf1  19594  0dgrb  19628  coe1termlem  19639  dgrcolem2  19655  plymul0or  19661  plyrem  19685  fta1  19688  quotcan  19689  aalioulem3  19714  eff1olem  19910  lognegb  19943  eflogeq  19955  argregt0  19964  argrege0  19965  tanarg  19970  cxpexp  20015  cxpeq0  20025  mulcxp  20032  cxpeq  20097  atans2  20227  scvxcvx  20280  isppw2  20353  vmappw  20354  vmacl  20356  efvmacl  20358  isnsqf  20373  mumullem2  20418  sqff1o  20420  dvdsppwf1o  20426  ppiublem1  20441  vmalelog  20444  chtublem  20450  fsumvma  20452  perfectlem2  20469  perfect  20470  bposlem1  20523  lgsmod  20560  lgsne0  20572  lgsdirnn0  20578  lgsqr  20585  lgsdchr  20587  lgseisenlem2  20589  lgsquadlem1  20593  lgsquadlem2  20594  2sqlem2  20603  mul2sq  20604  2sqlem7  20609  dchrisum0fno1  20660  pntrsumbnd2  20716  ostthlem1  20776  ostth2lem2  20783  ostth3  20787  ostth  20788  ismndo2  21012  ghgrplem1  21033  rngosn4  21094  nvmul0or  21210  ipasslem5  21413  ipasslem11  21418  hvmul0or  21604  his6  21678  hhssnv  21841  ocsh  21862  ocin  21875  shsidmi  21963  chnlen0  22023  h1de2bi  22133  h1de2ctlem  22134  h1de2ci  22135  spansni  22136  3oalem1  22241  nmcexi  22606  atcveq0  22928  chcv1  22935  cdjreui  23012  cdj3lem2b  23017  ballotlemfc0  23051  ballotlemfcc  23052  xrge0iifcnv  23315  xrge0tsmsd  23382  esumc  23430  esumpcvgval  23446  dmgmaddn0  23695  subfacp1lem4  23714  subfacp1lem5  23715  erdszelem8  23729  sconpi1  23770  cvmsss2  23805  cvmlift2lem12  23845  vdgr1a  23897  eupap1  23900  sinccvglem  24005  untsucf  24056  dfpo2  24112  dfrdg2  24152  trpred0  24239  wfrlem14  24269  wfrlem15  24270  frrlem4  24284  funpartfv  24483  colinearalg  24538  axpasch  24569  axlowdimlem16  24585  axlowdimlem17  24586  axlowdim  24589  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  colineardim1  24684  btwnconn1lem14  24723  segleantisym  24738  colinbtwnle  24741  outsidele  24755  lineunray  24770  linethru  24776  repfuntw  25160  repcpwti  25161  cbicp  25166  trran2  25393  ltrran2  25403  rltrran  25414  intfmu2  25519  cldifemp  25524  efilcp  25552  islimrs3  25581  trran  25614  addcanri  25666  intvconlem1  25703  vtarsuelt  25895  partarelt1  25896  clscnc  26010  elicc3  26228  opnregcld  26248  cldregopn  26249  fnejoin2  26318  unirep  26349  sdclem2  26452  ssbnd  26512  prdsbnd  26517  cntotbnd  26520  heibor1lem  26533  rrnequiv  26559  grpoeqdivid  26571  isdrngo3  26590  crngohomfo  26631  0idl  26650  1idl  26651  divrngidl  26653  smprngopr  26677  prnc  26692  ispridlc  26695  ralxpmap  26761  elrfi  26769  mrefg2  26782  eldiophb  26836  eldioph2b  26842  diophin  26852  diophun  26853  rexzrexnn0  26885  eldioph4b  26894  diophren  26896  rencldnfilem  26903  pellexlem6  26919  jm2.19  27086  rmydioph  27107  expdiophlem1  27114  expdioph  27116  dsmmacl  27207  dsmmlss  27210  lnr2i  27320  lpirlnr  27321  hbtlem2  27328  hbtlem4  27330  hbtlem6  27333  dgrsub2  27339  dgraa0p  27354  rngunsnply  27378  psgnunilem1  27416  psgnunilem2  27418  psgnghm  27437  hashgcdlem  27516  pm14.24  27632  addrcom  27680  dfafn5b  28023  bnj145  28755  lshpdisj  29177  lsateln0  29185  lsatcveq0  29222  opnlen0  29378  glb0N  29383  cmtbr4N  29445  cvrnbtwn2  29465  cvrnbtwn4  29469  atcvreq0  29504  cvlatexch1  29526  exatleN  29593  atlelt  29627  ps-2  29667  llnn0  29705  lplnn0N  29736  islpln2a  29737  lvoln0N  29780  islvol2aN  29781  4at  29802  dalemcea  29849  dalem3  29853  pmapglb2N  29960  pmapglb2xN  29961  cdlema1N  29980  cdlemb  29983  paddasslem17  30025  llnexchb2lem  30057  llnexchb2  30058  lhpat3  30235  ltrnid  30324  trlne  30374  cdlemc4  30383  cdleme11h  30455  cdlemednuN  30489  cdlemg1a  30759  tendoeq2  30963  tendoid0  31014  dva1dim  31174  dib1dim  31355  dihlatat  31527  dochkrshp4  31579  dochkr1  31668  lclkrlem2e  31701  lcfrlem16  31748  lcfrlem28  31760  mapd0  31855  hdmap14lem13  32073
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 177
  Copyright terms: Public domain W3C validator