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  4046  reusv2lem2  4639  reusv3  4645  alxfr  4650  reuhypd  4664  opth1  4710  euotd  4737  tz7.2  4852  ordtri1  4900  xpsspw  5104  fvmptdv2  5945  fveqressseq  6003  foco2  6027  fsn  6045  fnsnb  6066  fmptsng  6068  fmptsnd  6069  fconst2g  6102  fnprb  6106  funfvima  6122  soisoi  6199  isores3  6206  eusvobj2  6263  ovmpt2dv2  6409  f1opw2  6501  suppssfvOLD  6504  suppssov1OLD  6505  sorpssun  6560  sorpssin  6561  oneqmin  6613  nlimsucg  6650  onzsl  6654  tfinds  6667  funcnvuni  6726  opiota  6832  mpt2sn  6864  suppssov1  6924  suppssfv  6928  brtpos  6956  seqomlem1  7107  seqomlem2  7108  omordi  7207  omord  7209  omwordi  7212  oeeui  7243  nnmordi  7272  nnmord  7273  nnmwordi  7276  nnawordex  7278  nnaordex  7279  nneob  7293  omsmolem  7294  qsss  7364  eroveu  7398  mapsncnv  7458  ralxpmap  7461  elixpsn  7501  ixpsnf1o  7502  boxcutc  7505  pw2f1olem  7614  2pwne  7666  mapxpen  7676  mapunen  7679  php  7694  unxpdomlem2  7718  en1eqsnbi  7743  isfiniteg  7772  fofinf1o  7793  f1opwfi  7816  elfiun  7882  oieu  7956  brwdom2  7991  wdomtr  7993  ixpiunwdom  8009  en3lplem1  8022  suc11reg  8027  inf3lemd  8035  cantnfvalf  8075  cantnflt  8082  cantnfp1lem3  8090  cantnflem2  8100  cantnfltOLD  8112  cantnfp1lem3OLD  8116  r1tr  8185  dfac8alem  8401  wdomnumr  8436  isinfcard  8464  aceq3lem  8492  dfac5lem4  8498  dfac5  8500  dfac2  8502  coftr  8644  fin23lem28  8711  fin23lem29  8712  fin1a2lem11  8781  fin1a2lem12  8782  fin1a2lem13  8783  hsmexlem9  8796  axdclem  8890  pwcfsdom  8949  gchdomtri  8996  fpwwe2  9010  gchpwdom  9037  gchhar  9046  addnidpi  9268  nqereu  9296  genpv  9366  genpdm  9369  distrlem5pr  9394  mulid1  9582  ltne  9670  mul02  9747  cnegex  9750  mul0or  10185  sup2  10494  supmul1  10503  supmul  10506  creur  10525  creui  10526  cju  10527  nnsub  10570  un0addcl  10825  un0mulcl  10826  nn0sub  10842  elz2  10877  zaddcl  10900  suprzcl2  11173  qmulz  11186  qre  11188  qnegcl  11200  xrmax1  11379  xrmin2  11382  max1ALT  11390  xlesubadd  11458  xmulass  11482  xlemul1a  11483  xrsupexmnf  11499  xrinfmexpnf  11500  xrub  11506  iccid  11577  fzsn  11729  fzsuc2  11741  fz1sbc  11758  elfzp12  11761  seqid3  12136  bcval5  12381  bcpasc  12384  hashbnd  12396  hashnnn0genn0  12401  hashprg  12447  hashfzo  12474  wrdl1s1  12614  cats1un  12695  shftlem  12986  replim  13034  absmod0  13221  absz  13229  rlimdm  13459  summolem2  13623  summo  13624  zsum  13625  fsum  13627  fsummulc2  13684  fsumconst  13690  fsum00  13697  incexclem  13733  isumsplit  13737  infcvgaux1i  13753  prodmolem2  13827  prodmo  13828  zprod  13829  fprod  13833  prodsn  13852  fprodconst  13867  ruclem2  14052  fzo0dvdseq  14126  bitsf1ocnv  14181  sadcaddlem  14194  smueqlem  14227  gcdabs1  14259  bezoutlem1  14263  bezoutlem3  14265  bezoutlem4  14266  dvdsgcd  14268  dvdsmulgcd  14279  dvdsprime  14317  coprm  14328  isprm5  14340  prmdvdsexpr  14344  rpexp  14348  phibndlem  14387  dfphi2  14391  odzdvds  14409  pythagtriplem1  14427  iserodd  14446  pceulem  14456  pcqmul  14464  pcqcl  14467  pcxcl  14471  pcneg  14484  pcabs  14485  pcgcd1  14487  pcz  14491  pcprmpw2  14492  pcprmpw  14493  pcaddlem  14494  pcadd  14495  pcmpt  14498  pockthg  14511  prmreclem5  14525  4sqlem4  14557  mul4sq  14559  vdwapun  14579  vdwlem2  14587  vdwlem6  14591  vdwlem8  14593  vdwlem13  14598  0ram  14625  ram0  14627  ramcl  14634  cshwsiun  14671  wunress  14786  firest  14925  xpscfv  15054  isssc  15311  pospo  15805  latnlej  15900  gsumval2a  16108  mnd1id  16165  mulgnn0p1  16355  mulgnn0ass  16373  gicsubgen  16528  symg1bas  16623  psgnunilem1  16720  psgnunilem2  16722  mndodcongi  16769  oddvdsnn0  16770  odnncl  16771  oddvds  16773  odeq  16776  odeq1  16784  pgpfi2  16828  sylow2a  16841  sylow2blem3  16844  sylow3lem6  16854  lsmelvalm  16873  lsmsubm  16875  lsmsubg  16876  lsmmod  16895  lsmdisj2  16902  efgmnvl  16934  efgtlen  16946  efgs1b  16956  efgrelexlemb  16970  efgredeu  16972  efgcpbllemb  16975  frgpuptinv  16991  frgpup3lem  16997  qusabl  17073  frgpnabllem1  17079  cyggeninv  17088  cyggenod  17089  cygabl  17095  gsumval3eu  17109  dprdssv  17254  dprdfeq0  17260  dprdfeq0OLD  17267  dprdsubg  17269  dprddisj2  17285  dprddisj2OLD  17286  ablfacrp  17315  pgpfac1lem3  17326  pgpfaclem2  17331  dvreq1  17540  irredn1  17553  drngmul0or  17615  isabvd  17667  abvdom  17685  issrngd  17708  lss1d  17807  lspsneq0  17856  lbspss  17926  lsmcl  17927  lvecvs0or  17952  lspindpi  17976  lidl1el  18064  lpiss  18096  lidldvgen  18101  nzrunit  18113  rrgeq0  18136  domneq0  18144  mplsubrglem  18298  mplsubrglemOLD  18299  mplmonmul  18324  mplcoe5lem  18328  coe1tmmul2  18515  coe1tmmul  18516  pf1ind  18589  qsssubdrg  18675  zringlpirlem1  18700  znfld  18775  znunit  18778  znrrg  18780  cygznlem3  18784  frgpcyg  18788  psgnghm  18792  ipeq0  18849  cssincl  18895  lsmcss  18899  obselocv  18935  dsmmacl  18948  dsmmlss  18951  mat1dimelbas  19143  mdetralt  19280  mdetunilem2  19285  mdetunilem7  19290  mdetunilem9  19292  maducoeval2  19312  chpscmat  19513  chfacfscmulgsum  19531  chfacfpmmulgsum  19535  istopon  19596  eltg3  19633  tgidm  19652  clsval2  19721  opncldf1  19755  restbas  19829  tgrest  19830  restcld  19843  restcldr  19845  restcls  19852  restntr  19853  ordtbas2  19862  ordtbas  19863  ordtrest2lem  19874  ordtrest2  19875  pnfnei  19891  mnfnei  19892  tgcn  19923  cnconst  19955  cnindis  19963  lmss  19969  ordtt1  20050  discmp  20068  1stcrest  20123  2ndcdisj  20126  cldllycmp  20165  txbas  20237  ptpjpre1  20241  ptuni2  20246  ptbasin  20247  ptbasfi  20251  ptopn2  20254  txbasval  20276  ptpjopn  20282  ptclsg  20285  dfac14lem  20287  xkoccn  20289  ptcnp  20292  upxp  20293  ptrescn  20309  txkgen  20322  xkoptsub  20324  xkopt  20325  xkoco1cn  20327  xkoco2cn  20328  xkococn  20330  xkoinjcn  20357  ordthmeolem  20471  ptuncnv  20477  nrmhaus  20496  fbssint  20508  fbfinnfr  20511  fbasrn  20554  isufil2  20578  filufint  20590  rnelfm  20623  fmfnfmlem2  20625  fmfnfmlem3  20626  fmfnfmlem4  20627  fmfnfm  20628  flimtopon  20640  flimclslem  20654  fclstopon  20682  fclscf  20695  flimfnfcls  20698  alexsublem  20713  alexsubALTlem3  20718  alexsubALTlem4  20719  ptcmplem2  20722  tmdgsum2  20764  symgtgp  20769  cldsubg  20778  qustgplem  20788  tgptsmscld  20822  tsmsxplem1  20824  imasdsf1olem  21045  blssps  21096  blss  21097  stdbdxmet  21187  methaus  21192  metrest  21196  nrginvrcn  21369  nmoeq0  21412  blssioo  21469  xrtgioo  21480  xrsxmet  21483  reconnlem1  21500  reconnlem2  21501  xrge0tsms  21508  elcncf1di  21568  iccpnfcnv  21613  evth  21628  lebnumlem1  21630  lebnumlem2  21631  lebnumlem3  21632  nmoleub3  21771  minveclem3b  22012  ivthlem2  22033  ivthlem3  22034  elovolm  22055  ovolmge0  22057  ovoliun  22085  ovolicc2lem3  22099  ovolicc2  22102  voliunlem3  22131  dyaddisj  22174  dyadmax  22176  opnmblALT  22181  ismbfd  22216  ismbf2d  22217  mbfimaopnlem  22231  mbfimaopn2  22233  i1fmullem  22270  i1fres  22281  itg1climres  22290  mbfi1fseqlem4  22294  itg2lcl  22303  itgsplitioo  22413  ellimc2  22450  rolle  22560  dvlip  22563  dvge0  22576  dvne0  22581  lhop1lem  22583  tdeglem4  22627  degltlem1  22641  deg1nn0clb  22659  deg1lt0  22660  dvdsq1p  22730  ply1rem  22733  fta1g  22737  elply2  22762  plyf  22764  ne0p  22773  plyeq0lem  22776  plypf1  22778  0dgrb  22812  coe1termlem  22824  dgrcolem2  22840  plymul0or  22846  plyrem  22870  fta1  22873  quotcan  22874  aalioulem3  22899  eff1olem  23104  lognegb  23146  eflogeq  23158  argregt0  23166  argrege0  23167  tanarg  23175  cxpexp  23220  cxpeq0  23230  mulcxp  23237  cxpeq  23302  atans2  23462  scvxcvx  23516  isppw2  23590  vmappw  23591  vmacl  23593  efvmacl  23595  isnsqf  23610  mumullem2  23655  sqff1o  23657  dvdsppwf1o  23663  ppiublem1  23678  vmalelog  23681  chtublem  23687  fsumvma  23689  perfectlem2  23706  perfect  23707  bposlem1  23760  lgsmod  23797  lgsne0  23809  lgsdirnn0  23815  lgsqr  23822  lgsdchr  23824  lgseisenlem2  23826  lgsquadlem1  23830  lgsquadlem2  23831  2sqlem2  23840  mul2sq  23841  2sqlem7  23846  dchrisum0fno1  23897  pntrsumbnd2  23953  ostthlem1  24013  ostth2lem2  24020  ostth3  24024  ostth  24025  colinearalg  24418  axpasch  24449  axlowdimlem16  24465  axlowdimlem17  24466  axlowdim  24469  axcontlem2  24473  axcontlem4  24475  axcontlem7  24478  usgraexmpl  24606  nbgraf1olem1  24646  nbgraf1olem3  24648  nbgraf1olem5  24650  nb3graprlem2  24657  cusgrasize2inds  24682  wlklenvm1  24737  wlkiswwlksur  24924  wwlknextbi  24930  wwlkextproplem2  24947  clwlkisclwwlklem1  24992  clwwisshclww  25012  erclwwlktr  25020  erclwwlkntr  25032  clwlkfclwwlk1hash  25047  vdgr1a  25111  vdusgra0nedg  25113  usgravd0nedg  25123  0eusgraiff0rgra  25144  rusgraprop2  25147  eupap1  25181  vdn0frgrav2  25228  vdgn0frgrav2  25229  ismndo2  25548  ghgrplem1OLD  25569  nvmul0or  25748  ipasslem5  25951  ipasslem11  25956  hvmul0or  26143  his6  26217  hhssnv  26381  ocsh  26402  ocin  26415  shsidmi  26503  chnlen0  26563  h1de2bi  26673  h1de2ctlem  26674  h1de2ci  26675  spansni  26676  3oalem1  26781  nmcexi  27146  atcveq0  27468  chcv1  27475  cdjreui  27552  cdj3lem2b  27557  xrge0tsmsd  28013  ordtrest2NEWlem  28142  ordtrest2NEW  28143  xrge0iifcnv  28153  esumc  28283  esumpcvgval  28310  ballotlemfc0  28698  ballotlemfcc  28699  dmgmaddn0  28832  subfacp1lem4  28894  subfacp1lem5  28895  erdszelem8  28909  sconpi1  28951  cvmsss2  28986  cvmlift2lem12  29026  msubco  29158  msubvrs  29187  sinccvglem  29305  untsucf  29326  dfpo2  29428  dfrdg2  29471  trpred0  29562  wfrlem10  29595  wfrlem14  29599  wfrlem15  29600  frrlem4  29633  colineardim1  29942  btwnconn1lem14  29981  segleantisym  29996  colinbtwnle  29999  outsidele  30013  lineunray  30028  linethru  30034  supaddc  30284  supadd  30285  itg2addnclem3  30311  ftc1anclem6  30338  dvasin  30346  elicc3  30378  opnregcld  30391  cldregopn  30392  fnejoin2  30430  unirep  30446  sdclem2  30478  ssbnd  30527  prdsbnd  30532  cntotbnd  30535  heibor1lem  30548  rrnequiv  30574  grpoeqdivid  30586  isdrngo3  30605  crngohomfo  30646  0idl  30665  1idl  30666  divrngidl  30668  smprngopr  30692  prnc  30707  ispridlc  30710  elrfi  30869  mrefg2  30882  eldiophb  30932  eldioph2b  30938  diophin  30948  diophun  30949  rexzrexnn0  30980  eldioph4b  30987  diophren  30989  rencldnfilem  30996  pellexlem6  31012  jm2.19  31177  rmydioph  31198  expdiophlem1  31205  expdioph  31207  lnr2i  31309  lpirlnr  31310  hbtlem2  31317  hbtlem4  31319  hbtlem6  31322  dgrsub2  31328  dgraa0p  31342  rngunsnply  31366  hashgcdlem  31401  radcnvrat  31439  lcmgcdeq  31460  pm14.24  31583  addrcom  31628  prodsnf  31829  afveu  32480  dfafn5b  32488  rlimdmafv  32504  perfectALTVlem2  32616  perfectALTV  32617  proththdlem  32619  uhgrauhg  32764  lincellss  33300  lindsrng01  33342  suppdm  33385  nnpw2pb  33481  bnj145OLD  34202  riotaclbgBAD  35101  lshpdisj  35128  lsateln0  35136  lsatcveq0  35173  opnlen0  35329  cmtbr4N  35396  cvrnbtwn2  35416  cvrnbtwn4  35420  atcvreq0  35455  cvlatexch1  35477  exatleN  35544  atlelt  35578  ps-2  35618  llnn0  35656  lplnn0N  35687  islpln2a  35688  lvoln0N  35731  islvol2aN  35732  4at  35753  dalemcea  35800  dalem3  35804  pmapglb2N  35911  pmapglb2xN  35912  cdlema1N  35931  cdlemb  35934  paddasslem17  35976  llnexchb2lem  36008  llnexchb2  36009  lhpat3  36186  ltrnid  36275  trlne  36326  cdlemc4  36335  cdleme11h  36407  cdlemednuN  36441  cdlemg1a  36712  tendoeq2  36916  tendoid0  36967  dva1dim  37127  dib1dim  37308  dihlatat  37480  dochkrshp4  37532  dochkr1  37621  lclkrlem2e  37654  lcfrlem16  37701  lcfrlem28  37713  mapd0  37808  hdmap14lem13  38026
  Copyright terms: Public domain W3C validator