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  4057  reusv2lem2  4649  reusv3  4655  alxfr  4660  reuhypd  4674  opth1  4720  euotd  4748  tz7.2  4863  ordtri1  4911  xpsspw  5114  fvmptdv2  5961  foco2  6039  fsn  6057  fnsnb  6078  fmptsng  6080  fmptsnd  6081  fconst2g  6113  fnprb  6117  fnprOLD  6118  funfvima  6133  soisoi  6210  isores3  6217  eusvobj2  6275  ovmpt2dv2  6418  f1opw2  6510  suppssfvOLD  6513  suppssov1OLD  6514  sorpssun  6569  sorpssin  6570  oneqmin  6618  nlimsucg  6655  onzsl  6659  tfinds  6672  funcnvuni  6734  opiota  6840  mpt2sn  6871  suppssov1  6929  suppssfv  6933  brtpos  6961  seqomlem1  7112  seqomlem2  7113  omordi  7212  omord  7214  omwordi  7217  oeeui  7248  nnmordi  7277  nnmord  7278  nnmwordi  7281  nnawordex  7283  nnaordex  7284  nneob  7298  omsmolem  7299  qsss  7369  eroveu  7403  mapsncnv  7462  ralxpmap  7465  elixpsn  7505  ixpsnf1o  7506  boxcutc  7509  pw2f1olem  7618  2pwne  7670  mapxpen  7680  mapunen  7683  php  7698  unxpdomlem2  7722  isfiniteg  7776  fofinf1o  7797  f1opwfi  7820  elfiun  7886  oieu  7960  brwdom2  7995  wdomtr  7997  ixpiunwdom  8013  en3lplem1  8027  suc11reg  8032  inf3lemd  8040  cantnfvalf  8080  cantnflt  8087  cantnfp1lem3  8095  cantnflem2  8105  cantnfltOLD  8117  cantnfp1lem3OLD  8121  r1tr  8190  dfac8alem  8406  wdomnumr  8441  isinfcard  8469  aceq3lem  8497  dfac5lem4  8503  dfac5  8505  dfac2  8507  coftr  8649  fin23lem28  8716  fin23lem29  8717  fin1a2lem11  8786  fin1a2lem12  8787  fin1a2lem13  8788  hsmexlem9  8801  axdclem  8895  pwcfsdom  8954  gchdomtri  9003  fpwwe2  9017  gchpwdom  9044  gchhar  9053  addnidpi  9275  nqereu  9303  genpv  9373  genpdm  9376  distrlem5pr  9401  mulid1  9589  ltne  9677  mul02  9753  cnegex  9756  mul0or  10185  sup2  10495  supmul1  10504  supmul  10507  creur  10526  creui  10527  cju  10528  nnsub  10570  un0addcl  10825  un0mulcl  10826  nn0sub  10842  elz2  10877  zaddcl  10899  suprzcl2  11168  qmulz  11181  qre  11183  qnegcl  11195  xrmax1  11372  xrmin2  11375  max1ALT  11383  xlesubadd  11451  xmulass  11475  xlemul1a  11476  xrsupexmnf  11492  xrinfmexpnf  11493  xrub  11499  iccid  11570  fzsn  11721  fzsuc2  11733  fz1sbc  11750  elfzp12  11753  fzm1  11754  seqid3  12115  bcval5  12360  bcpasc  12363  hashbnd  12375  hashnnn0genn0  12380  hashprg  12424  hashfzo  12448  wrdl1s1  12581  cats1un  12660  shftlem  12860  replim  12908  absmod0  13095  absz  13103  rlimdm  13333  summolem2  13497  summo  13498  zsum  13499  fsum  13501  fsummulc2  13558  fsumconst  13564  fsum00  13571  incexclem  13607  isumsplit  13611  infcvgaux1i  13627  ruclem2  13822  fzo0dvdseq  13894  bitsf1ocnv  13949  sadcaddlem  13962  smueqlem  13995  gcdabs1  14027  bezoutlem1  14031  bezoutlem3  14033  bezoutlem4  14034  dvdsgcd  14036  dvdsmulgcd  14047  dvdsprime  14085  coprm  14096  isprm5  14108  prmdvdsexpr  14112  rpexp  14116  phibndlem  14155  dfphi2  14159  odzdvds  14177  pythagtriplem1  14195  iserodd  14214  pceulem  14224  pcqmul  14232  pcqcl  14235  pcxcl  14239  pcneg  14252  pcabs  14253  pcgcd1  14255  pcz  14259  pcprmpw2  14260  pcprmpw  14261  pcaddlem  14262  pcadd  14263  pcmpt  14266  pockthg  14279  prmreclem5  14293  4sqlem4  14325  mul4sq  14327  vdwapun  14347  vdwlem2  14355  vdwlem6  14359  vdwlem8  14361  vdwlem13  14366  0ram  14393  ram0  14395  ramcl  14402  cshwsiun  14438  wunress  14550  firest  14684  xpscfv  14813  isssc  15046  pospo  15456  latnlej  15551  gsumval2a  15825  mulgnn0p1  15953  mulgnn0ass  15971  gicsubgen  16121  symg1bas  16216  psgnunilem1  16314  psgnunilem2  16316  mndodcongi  16363  oddvdsnn0  16364  odnncl  16365  oddvds  16367  odeq  16370  odeq1  16378  pgpfi2  16422  sylow2a  16435  sylow2blem3  16438  sylow3lem6  16448  lsmelvalm  16467  lsmsubm  16469  lsmsubg  16470  lsmmod  16489  lsmdisj2  16496  efgmnvl  16528  efgtlen  16540  efgs1b  16550  efgrelexlemb  16564  efgredeu  16566  efgcpbllemb  16569  frgpuptinv  16585  frgpup3lem  16591  divsabl  16664  frgpnabllem1  16668  cyggeninv  16677  cyggenod  16678  cygabl  16684  gsumval3eu  16698  dprdssv  16846  dprdfeq0  16852  dprdfeq0OLD  16859  dprdsubg  16861  dprddisj2  16877  dprddisj2OLD  16878  ablfacrp  16907  pgpfac1lem3  16918  pgpfaclem2  16923  dvreq1  17126  irredn1  17139  drngmul0or  17200  isabvd  17252  abvdom  17270  issrngd  17293  lss1d  17392  lspsneq0  17441  lbspss  17511  lsmcl  17512  lvecvs0or  17537  lspindpi  17561  lidl1el  17648  lpiss  17680  lidldvgen  17685  nzrunit  17696  rrgeq0  17709  domneq0  17717  mplsubrglem  17871  mplsubrglemOLD  17872  mplmonmul  17897  mplcoe5lem  17901  coe1tmmul2  18088  coe1tmmul  18089  pf1ind  18162  qsssubdrg  18245  zringlpirlem1  18276  zlpirlem1  18281  znfld  18366  znunit  18369  znrrg  18371  cygznlem3  18375  frgpcyg  18379  psgnghm  18383  ipeq0  18440  cssincl  18486  lsmcss  18490  obselocv  18526  dsmmacl  18539  dsmmlss  18542  mat1dimelbas  18740  mdetralt  18877  mdetunilem2  18882  mdetunilem7  18887  mdetunilem9  18889  maducoeval2  18909  chpscmat  19110  chfacfscmulgsum  19128  chfacfpmmulgsum  19132  istopon  19193  eltg3  19230  tgidm  19248  clsval2  19317  opncldf1  19351  restbas  19425  tgrest  19426  restcld  19439  restcldr  19441  restcls  19448  restntr  19449  ordtbas2  19458  ordtbas  19459  ordtrest2lem  19470  ordtrest2  19471  pnfnei  19487  mnfnei  19488  tgcn  19519  cnconst  19551  cnindis  19559  lmss  19565  ordtt1  19646  discmp  19664  1stcrest  19720  2ndcdisj  19723  cldllycmp  19762  txbas  19803  ptpjpre1  19807  ptuni2  19812  ptbasin  19813  ptbasfi  19817  ptopn2  19820  txbasval  19842  ptpjopn  19848  ptclsg  19851  dfac14lem  19853  xkoccn  19855  ptcnp  19858  upxp  19859  ptrescn  19875  txkgen  19888  xkoptsub  19890  xkopt  19891  xkoco1cn  19893  xkoco2cn  19894  xkococn  19896  xkoinjcn  19923  ordthmeolem  20037  ptuncnv  20043  nrmhaus  20062  fbssint  20074  fbfinnfr  20077  fbasrn  20120  isufil2  20144  filufint  20156  rnelfm  20189  fmfnfmlem2  20191  fmfnfmlem3  20192  fmfnfmlem4  20193  fmfnfm  20194  flimtopon  20206  flimclslem  20220  fclstopon  20248  fclscf  20261  flimfnfcls  20264  alexsublem  20279  alexsubALTlem3  20284  alexsubALTlem4  20285  ptcmplem2  20288  tmdgsum2  20330  symgtgp  20335  cldsubg  20344  divstgplem  20354  tgptsmscld  20388  tsmsxplem1  20390  imasdsf1olem  20611  blssps  20662  blss  20663  stdbdxmet  20753  methaus  20758  metrest  20762  nrginvrcn  20935  nmoeq0  20978  blssioo  21035  xrtgioo  21046  xrsxmet  21049  reconnlem1  21066  reconnlem2  21067  xrge0tsms  21074  elcncf1di  21134  iccpnfcnv  21179  evth  21194  lebnumlem1  21196  lebnumlem2  21197  lebnumlem3  21198  nmoleub3  21337  minveclem3b  21578  ivthlem2  21599  ivthlem3  21600  elovolm  21621  ovolmge0  21623  ovoliun  21651  ovolicc2lem3  21665  ovolicc2  21668  voliunlem3  21697  dyaddisj  21740  dyadmax  21742  opnmblALT  21747  ismbfd  21782  ismbf2d  21783  mbfimaopnlem  21797  mbfimaopn2  21799  i1fmullem  21836  i1fres  21847  itg1climres  21856  mbfi1fseqlem4  21860  itg2lcl  21869  itgsplitioo  21979  ellimc2  22016  rolle  22126  dvlip  22129  dvge0  22142  dvne0  22147  lhop1lem  22149  tdeglem4  22193  degltlem1  22207  deg1nn0clb  22225  deg1lt0  22226  dvdsq1p  22296  ply1rem  22299  fta1g  22303  elply2  22328  plyf  22330  ne0p  22339  plyeq0lem  22342  plypf1  22344  0dgrb  22378  coe1termlem  22389  dgrcolem2  22405  plymul0or  22411  plyrem  22435  fta1  22438  quotcan  22439  aalioulem3  22464  eff1olem  22668  lognegb  22702  eflogeq  22714  argregt0  22723  argrege0  22724  tanarg  22732  cxpexp  22777  cxpeq0  22787  mulcxp  22794  cxpeq  22859  atans2  22990  scvxcvx  23043  isppw2  23117  vmappw  23118  vmacl  23120  efvmacl  23122  isnsqf  23137  mumullem2  23182  sqff1o  23184  dvdsppwf1o  23190  ppiublem1  23205  vmalelog  23208  chtublem  23214  fsumvma  23216  perfectlem2  23233  perfect  23234  bposlem1  23287  lgsmod  23324  lgsne0  23336  lgsdirnn0  23342  lgsqr  23349  lgsdchr  23351  lgseisenlem2  23353  lgsquadlem1  23357  lgsquadlem2  23358  2sqlem2  23367  mul2sq  23368  2sqlem7  23373  dchrisum0fno1  23424  pntrsumbnd2  23480  ostthlem1  23540  ostth2lem2  23547  ostth3  23551  ostth  23552  colinearalg  23889  axpasch  23920  axlowdimlem16  23936  axlowdimlem17  23937  axlowdim  23940  axcontlem2  23944  axcontlem4  23946  axcontlem7  23949  usgraexmpl  24077  nbgraf1olem1  24117  nbgraf1olem3  24119  nbgraf1olem5  24121  nb3graprlem2  24128  cusgrasize2inds  24153  wlklenvm1  24208  wlklniswwlkn2  24376  wlkiswwlksur  24395  wwlknextbi  24401  wwlkextproplem2  24418  clwlkisclwwlklem1  24463  clwwisshclww  24483  erclwwlktr  24491  erclwwlkntr  24503  clwlkfclwwlk1hash  24518  vdgr1a  24582  vdusgra0nedg  24584  usgravd0nedg  24594  0eusgraiff0rgra  24615  rusgraprop2  24618  eupap1  24652  vdn0frgrav2  24700  vdgn0frgrav2  24701  ismndo2  25023  ghgrplem1  25044  rngosn4  25105  nvmul0or  25223  ipasslem5  25426  ipasslem11  25431  hvmul0or  25618  his6  25692  hhssnv  25856  ocsh  25877  ocin  25890  shsidmi  25978  chnlen0  26038  h1de2bi  26148  h1de2ctlem  26149  h1de2ci  26150  spansni  26151  3oalem1  26256  nmcexi  26621  atcveq0  26943  chcv1  26950  cdjreui  27027  cdj3lem2b  27032  xrge0tsmsd  27438  ordtrest2NEWlem  27540  ordtrest2NEW  27541  xrge0iifcnv  27551  esumc  27702  esumpcvgval  27724  ballotlemfc0  28071  ballotlemfcc  28072  dmgmaddn0  28205  subfacp1lem4  28267  subfacp1lem5  28268  erdszelem8  28282  sconpi1  28324  cvmsss2  28359  cvmlift2lem12  28399  sinccvglem  28513  untsucf  28557  prodmolem2  28644  prodmo  28645  zprod  28646  fprod  28650  prodsn  28669  fprodconst  28685  dfpo2  28761  dfrdg2  28805  trpred0  28896  wfrlem10  28929  wfrlem14  28933  wfrlem15  28934  frrlem4  28967  colineardim1  29288  btwnconn1lem14  29327  segleantisym  29342  colinbtwnle  29345  outsidele  29359  lineunray  29374  linethru  29380  supaddc  29618  supadd  29619  itg2addnclem3  29645  ftc1anclem6  29672  dvasin  29680  elicc3  29712  opnregcld  29725  cldregopn  29726  fnejoin2  29790  unirep  29806  sdclem2  29838  ssbnd  29887  prdsbnd  29892  cntotbnd  29895  heibor1lem  29908  rrnequiv  29934  grpoeqdivid  29946  isdrngo3  29965  crngohomfo  30006  0idl  30025  1idl  30026  divrngidl  30028  smprngopr  30052  prnc  30067  ispridlc  30070  elrfi  30230  mrefg2  30243  eldiophb  30294  eldioph2b  30300  diophin  30310  diophun  30311  rexzrexnn0  30341  eldioph4b  30349  diophren  30351  rencldnfilem  30358  pellexlem6  30374  jm2.19  30539  rmydioph  30560  expdiophlem1  30567  expdioph  30569  lnr2i  30669  lpirlnr  30670  hbtlem2  30677  hbtlem4  30679  hbtlem6  30682  dgrsub2  30688  dgraa0p  30703  rngunsnply  30727  hashgcdlem  30762  lcmgcdeq  30816  pm14.24  30917  addrcom  30962  afveu  31705  dfafn5b  31713  rlimdmafv  31729  uhgrauhg  31842  lincellss  32100  lindsrng01  32142  bnj145OLD  32862  riotaclbgBAD  33757  riotaclbBAD  33758  lshpdisj  33784  lsateln0  33792  lsatcveq0  33829  opnlen0  33985  cmtbr4N  34052  cvrnbtwn2  34072  cvrnbtwn4  34076  atcvreq0  34111  cvlatexch1  34133  exatleN  34200  atlelt  34234  ps-2  34274  llnn0  34312  lplnn0N  34343  islpln2a  34344  lvoln0N  34387  islvol2aN  34388  4at  34409  dalemcea  34456  dalem3  34460  pmapglb2N  34567  pmapglb2xN  34568  cdlema1N  34587  cdlemb  34590  paddasslem17  34632  llnexchb2lem  34664  llnexchb2  34665  lhpat3  34842  ltrnid  34931  trlne  34981  cdlemc4  34990  cdleme11h  35062  cdlemednuN  35096  cdlemg1a  35366  tendoeq2  35570  tendoid0  35621  dva1dim  35781  dib1dim  35962  dihlatat  36134  dochkrshp4  36186  dochkr1  36275  lclkrlem2e  36308  lcfrlem16  36355  lcfrlem28  36367  mapd0  36462  hdmap14lem13  36680
  Copyright terms: Public domain W3C validator