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  2019  elsnc2g  3669  opth1  4243  euotd  4266  tz7.2  4376  ordtri1  4424  reusv2lem2  4535  reusv3  4541  alxfr  4546  reuhypd  4560  oneqmin  4595  nlimsucg  4632  onzsl  4636  tfinds  4649  xpsspw  4796  funcnvuni  5283  fvmptdv2  5575  foco2  5642  fsn  5658  fconst2g  5690  funfvima  5715  soisoi  5787  isores3  5794  ovmpt2dv2  5943  f1opw2  6033  suppssfv  6036  suppssov1  6037  brtpos  6205  sorpssun  6246  sorpssin  6247  opiota  6284  eusvobj2  6333  riotaclbg  6340  seqomlem1  6458  seqomlem2  6459  omordi  6560  omord  6562  omwordi  6565  oeeui  6596  nnmordi  6625  nnmord  6626  nnmwordi  6629  nnawordex  6631  nnaordex  6632  nneob  6646  omsmolem  6647  qsss  6716  eroveu  6749  th3qlem1  6760  mapsncnv  6810  elixpsn  6851  ixpsnf1o  6852  boxcutc  6855  pw2f1olem  6962  2pwne  7013  mapxpen  7023  mapunen  7026  php  7041  unxpdomlem2  7064  isfiniteg  7113  fofinf1o  7133  f1opwfi  7155  elfiun  7179  oieu  7250  brwdom2  7283  wdomtr  7285  ixpiunwdom  7301  suc11reg  7316  inf3lemd  7324  cantnfvalf  7362  cantnflt  7369  cantnfp1lem3  7378  cantnflem2  7388  en3lplem1  7412  r1tr  7444  dfac8alem  7652  wdomnumr  7687  isinfcard  7715  aceq3lem  7743  dfac5lem4  7749  dfac5  7751  dfac2  7753  coftr  7895  fin23lem28  7962  fin23lem29  7963  fin1a2lem11  8032  fin1a2lem12  8033  fin1a2lem13  8034  hsmexlem9  8047  axdclem  8142  pwcfsdom  8201  gchdomtri  8247  fpwwe2  8261  gchhar  8289  gchpwdom  8292  addnidpi  8521  nqereu  8549  genpv  8619  genpdm  8622  distrlem5pr  8647  mulid1  8831  ltne  8913  mul02  8986  cnegex  8989  mul0or  9404  sup2  9706  supmul1  9715  supmul  9718  creur  9736  creui  9737  cju  9738  nnsub  9780  un0addcl  9993  un0mulcl  9994  nn0sub  10010  elz2  10036  zaddcl  10055  suprzcl2  10304  qmulz  10315  qre  10317  qnegcl  10329  xrmax1  10500  xrmin2  10503  max1ALT  10511  xlesubadd  10579  xmulass  10603  xlemul1a  10604  xrsupexmnf  10619  xrinfmexpnf  10620  xrub  10626  iccid  10697  fzsn  10829  fzsuc2  10838  fz1sbc  10855  elfzp12  10857  fzm1  10858  seqid3  11086  bcval5  11326  bcpasc  11329  hashbnd  11339  hashprg  11364  hashfzo  11379  cats1un  11472  shftlem  11559  replim  11597  absmod0  11784  absz  11792  rlimdm  12021  summolem2  12185  summo  12186  zsum  12187  fsum  12189  fsummulc2  12242  fsumconst  12248  fsum00  12252  incexclem  12291  isumsplit  12295  infcvgaux1i  12311  ruclem2  12506  fzo0dvdseq  12577  bitsf1ocnv  12631  sadcaddlem  12644  smueqlem  12677  gcdabs1  12709  bezoutlem1  12713  bezoutlem3  12715  bezoutlem4  12716  dvdsgcd  12718  dvdsmulgcd  12729  dvdsprime  12767  coprm  12775  isprm5  12787  prmdvdsexpr  12791  rpexp  12795  phibndlem  12834  dfphi2  12838  odzdvds  12856  pythagtriplem1  12865  iserodd  12884  pceulem  12894  pcqmul  12902  pcqcl  12905  pcxcl  12909  pcneg  12922  pcabs  12923  pcgcd1  12925  pcz  12929  pcprmpw2  12930  pcprmpw  12931  pcaddlem  12932  pcadd  12933  pcmpt  12936  pockthg  12949  prmreclem5  12963  4sqlem4  12995  mul4sq  12997  vdwapun  13017  vdwlem2  13025  vdwlem6  13029  vdwlem8  13031  vdwlem13  13036  0ram  13063  ram0  13065  ramcl  13072  wunress  13203  firest  13333  xpscfv  13460  isssc  13693  pospo  14103  latnlej  14170  gsumval2a  14455  mulgnn0p1  14574  mulgnn0ass  14592  gicsubgen  14738  mndodcongi  14854  oddvdsnn0  14855  odnncl  14856  oddvds  14858  odeq  14861  odeq1  14869  pgpfi2  14913  sylow2a  14926  sylow2blem3  14929  sylow3lem6  14939  lsmelvalm  14958  lsmsubm  14960  lsmsubg  14961  lsmmod  14980  lsmdisj2  14987  efgmnvl  15019  efgtlen  15031  efgs1b  15041  efgrelexlemb  15055  efgredeu  15057  efgcpbllemb  15060  frgpuptinv  15076  frgpup3lem  15082  divsabl  15153  frgpnabllem1  15157  cyggeninv  15166  cyggenod  15167  cygabl  15173  gsumval3eu  15186  dprdssv  15247  dprdfeq0  15253  dprdsubg  15255  dprddisj2  15270  ablfacrp  15297  pgpfac1lem3  15308  pgpfaclem2  15313  dvreq1  15471  irredn1  15484  drngmul0or  15529  isabvd  15581  abvdom  15599  issrngd  15622  lss1d  15716  lspsneq0  15765  lbspss  15831  lsmcl  15832  lvecvs0or  15857  lspindpi  15881  lidl1el  15966  lpiss  15998  lidldvgen  16003  nzrunit  16014  rrgeq0  16027  domneq0  16034  mplsubrglem  16179  mplmonmul  16204  coe1tmmul2  16348  coe1tmmul  16349  qsssubdrg  16427  zlpirlem1  16437  znfld  16510  znunit  16513  znrrg  16515  cygznlem3  16519  frgpcyg  16523  ipeq0  16538  cssincl  16584  lsmcss  16588  obselocv  16624  istopon  16659  eltg3  16696  tgidm  16714  clsval2  16783  opncldf1  16817  restbas  16885  tgrest  16886  restcld  16899  restcldr  16901  restcls  16907  restntr  16908  ordtbas2  16917  ordtbas  16918  ordtrest2lem  16929  ordtrest2  16930  pnfnei  16946  mnfnei  16947  tgcn  16978  cnconst  17008  cnindis  17016  lmss  17022  ordtt1  17103  discmp  17121  1stcrest  17175  2ndcdisj  17178  cldllycmp  17217  txbas  17258  ptpjpre1  17262  ptuni2  17267  ptbasin  17268  ptbasfi  17272  ptopn2  17275  txbasval  17297  ptpjopn  17302  ptclsg  17305  dfac14lem  17307  xkoccn  17309  ptcnp  17312  upxp  17313  ptrescn  17329  txkgen  17342  xkoptsub  17344  xkopt  17345  xkoco1cn  17347  xkoco2cn  17348  xkococn  17350  xkoinjcn  17377  ordthmeolem  17488  ptuncnv  17494  nrmhaus  17513  fbssint  17529  fbfinnfr  17532  fbasrn  17575  isufil2  17599  filufint  17611  rnelfm  17644  fmfnfmlem2  17646  fmfnfmlem3  17647  fmfnfmlem4  17648  fmfnfm  17649  flimtopon  17661  flimclslem  17675  fclstopon  17703  fclscf  17716  flimfnfcls  17719  alexsublem  17734  alexsubALTlem3  17739  alexsubALTlem4  17740  ptcmplem2  17743  tmdgsum2  17775  symgtgp  17780  cldsubg  17789  divstgplem  17799  tgptsmscld  17829  tsmsxplem1  17831  imasdsf1olem  17933  blss  17968  stdbdxmet  18057  methaus  18062  metrest  18066  nrginvrcn  18198  nmoeq0  18241  blssioo  18297  xrtgioo  18308  xrsxmet  18311  reconnlem1  18327  reconnlem2  18328  xrge0tsms  18335  elcncf1di  18395  iccpnfcnv  18438  evth  18453  lebnumlem1  18455  lebnumlem2  18456  lebnumlem3  18457  nmoleub3  18596  minveclem3b  18788  ivthlem2  18808  ivthlem3  18809  elovolm  18830  ovolmge0  18832  ovoliun  18860  ovolicc2lem3  18874  ovolicc2  18877  voliunlem3  18905  dyaddisj  18947  dyadmax  18949  opnmblALT  18954  ismbfd  18991  ismbf2d  18992  mbfimaopnlem  19006  mbfimaopn2  19008  i1fmullem  19045  i1fres  19056  itg1climres  19065  mbfi1fseqlem4  19069  itg2lcl  19078  itgsplitioo  19188  ellimc2  19223  rolle  19333  dvlip  19336  dvge0  19349  dvne0  19354  lhop1lem  19356  pf1ind  19434  tdeglem4  19442  degltlem1  19454  deg1nn0clb  19472  deg1lt0  19473  dvdsq1p  19542  ply1rem  19545  fta1g  19549  elply2  19574  plyf  19576  ne0p  19585  plyeq0lem  19588  plypf1  19590  0dgrb  19624  coe1termlem  19635  dgrcolem2  19651  plymul0or  19657  plyrem  19681  fta1  19684  quotcan  19685  aalioulem3  19710  eff1olem  19906  lognegb  19939  eflogeq  19951  argregt0  19960  argrege0  19961  tanarg  19966  cxpexp  20011  cxpeq0  20021  mulcxp  20028  cxpeq  20093  atans2  20223  scvxcvx  20276  isppw2  20349  vmappw  20350  vmacl  20352  efvmacl  20354  isnsqf  20369  mumullem2  20414  sqff1o  20416  dvdsppwf1o  20422  ppiublem1  20437  vmalelog  20440  chtublem  20446  fsumvma  20448  perfectlem2  20465  perfect  20466  bposlem1  20519  lgsmod  20556  lgsne0  20568  lgsdirnn0  20574  lgsqr  20581  lgsdchr  20583  lgseisenlem2  20585  lgsquadlem1  20589  lgsquadlem2  20590  2sqlem2  20599  mul2sq  20600  2sqlem7  20605  dchrisum0fno1  20656  pntrsumbnd2  20712  ostthlem1  20772  ostth2lem2  20779  ostth3  20783  ostth  20784  ismndo2  21006  ghgrplem1  21027  rngosn4  21088  nvmul0or  21204  ipasslem5  21407  ipasslem11  21412  hvmul0or  21600  his6  21674  hhssnv  21837  ocsh  21858  ocin  21871  shsidmi  21959  chnlen0  22019  h1de2bi  22129  h1de2ctlem  22130  h1de2ci  22131  spansni  22132  3oalem1  22237  nmcexi  22602  atcveq0  22924  chcv1  22931  cdjreui  23008  cdj3lem2b  23013  ballotlemfc0  23047  ballotlemfcc  23048  dmgmaddn0  23102  subfacp1lem4  23121  subfacp1lem5  23122  erdszelem8  23136  sconpi1  23177  cvmsss2  23212  cvmlift2lem12  23252  vdgr1a  23304  eupap1  23307  sinccvglem  23412  untsucf  23463  dfpo2  23518  dfrdg2  23556  trpred0  23643  wfrlem14  23673  wfrlem15  23674  frrlem4  23688  axfelem18  23767  axfelem20  23769  funpartfv  23893  colinearalg  23948  axpasch  23979  axlowdimlem16  23995  axlowdimlem17  23996  axlowdim  23999  axcontlem2  24003  axcontlem4  24005  axcontlem7  24008  colineardim1  24094  btwnconn1lem14  24133  segleantisym  24148  colinbtwnle  24151  outsidele  24165  lineunray  24180  linethru  24186  repcpwti  24572  cbicp  24577  trran2  24804  ltrran2  24814  rltrran  24825  intfmu2  24930  cldifemp  24935  efilcp  24963  islimrs3  24992  trran  25025  addcanri  25077  intvconlem1  25114  vtarsuelt  25306  partarelt1  25307  clscnc  25421  elicc3  25639  opnregcld  25659  cldregopn  25660  fnejoin2  25729  unirep  25760  sdclem2  25863  ssbnd  25923  prdsbnd  25928  cntotbnd  25931  heibor1lem  25944  rrnequiv  25970  grpoeqdivid  25982  isdrngo3  26001  crngohomfo  26042  0idl  26061  1idl  26062  divrngidl  26064  smprngopr  26088  prnc  26103  ispridlc  26106  ralxpmap  26172  elrfi  26180  mrefg2  26193  eldiophb  26247  eldioph2b  26253  diophin  26263  diophun  26264  rexzrexnn0  26296  eldioph4b  26305  diophren  26307  rencldnfilem  26314  pellexlem6  26330  jm2.19  26497  rmydioph  26518  expdiophlem1  26525  expdioph  26527  dsmmacl  26618  dsmmlss  26621  lnr2i  26731  lpirlnr  26732  hbtlem2  26739  hbtlem4  26741  hbtlem6  26744  dgrsub2  26750  dgraa0p  26765  rngunsnply  26789  psgnunilem1  26827  psgnunilem2  26829  psgnghm  26848  hashgcdlem  26927  pm14.24  27043  addrcom  27091  dfafn5b  27414  bnj145  28034  lshpdisj  28456  lsateln0  28464  lsatcveq0  28501  opnlen0  28657  glb0N  28662  cmtbr4N  28724  cvrnbtwn2  28744  cvrnbtwn4  28748  atcvreq0  28783  cvlatexch1  28805  exatleN  28872  atlelt  28906  ps-2  28946  llnn0  28984  lplnn0N  29015  islpln2a  29016  lvoln0N  29059  islvol2aN  29060  4at  29081  dalemcea  29128  dalem3  29132  pmapglb2N  29239  pmapglb2xN  29240  cdlema1N  29259  cdlemb  29262  paddasslem17  29304  llnexchb2lem  29336  llnexchb2  29337  lhpat3  29514  ltrnid  29603  trlne  29653  cdlemc4  29662  cdleme11h  29734  cdlemednuN  29768  cdlemg1a  30038  tendoeq2  30242  tendoid0  30293  dva1dim  30453  dib1dim  30634  dihlatat  30806  dochkrshp4  30858  dochkr1  30947  lclkrlem2e  30980  lcfrlem16  31027  lcfrlem28  31039  mapd0  31134  hdmap14lem13  31352
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