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  3912  reusv2lem2  4499  reusv3  4505  alxfr  4510  reuhypd  4524  opth1  4570  euotd  4597  tz7.2  4709  ordtri1  4757  xpsspw  4958  fvmptdv2  5792  foco2  5868  fsn  5886  fnsnb  5903  fmptsng  5905  fconst2g  5937  fnprb  5941  fnprOLD  5942  funfvima  5957  soisoi  6024  isores3  6031  eusvobj2  6089  ovmpt2dv2  6229  f1opw2  6318  suppssfvOLD  6321  suppssov1OLD  6322  sorpssun  6372  sorpssin  6373  oneqmin  6421  nlimsucg  6458  onzsl  6462  tfinds  6475  funcnvuni  6535  opiota  6638  suppssov1  6726  suppssfv  6730  brtpos  6759  seqomlem1  6910  seqomlem2  6911  omordi  7010  omord  7012  omwordi  7015  oeeui  7046  nnmordi  7075  nnmord  7076  nnmwordi  7079  nnawordex  7081  nnaordex  7082  nneob  7096  omsmolem  7097  qsss  7166  eroveu  7200  th3qlem1  7211  mapsncnv  7264  ralxpmap  7267  elixpsn  7307  ixpsnf1o  7308  boxcutc  7311  pw2f1olem  7420  2pwne  7472  mapxpen  7482  mapunen  7485  php  7500  unxpdomlem2  7523  isfiniteg  7577  fofinf1o  7597  f1opwfi  7620  elfiun  7685  oieu  7758  brwdom2  7793  wdomtr  7795  ixpiunwdom  7811  en3lplem1  7825  suc11reg  7830  inf3lemd  7838  cantnfvalf  7878  cantnflt  7885  cantnfp1lem3  7893  cantnflem2  7903  cantnfltOLD  7915  cantnfp1lem3OLD  7919  r1tr  7988  dfac8alem  8204  wdomnumr  8239  isinfcard  8267  aceq3lem  8295  dfac5lem4  8301  dfac5  8303  dfac2  8305  coftr  8447  fin23lem28  8514  fin23lem29  8515  fin1a2lem11  8584  fin1a2lem12  8585  fin1a2lem13  8586  hsmexlem9  8599  axdclem  8693  pwcfsdom  8752  gchdomtri  8801  fpwwe2  8815  gchpwdom  8842  gchhar  8851  addnidpi  9075  nqereu  9103  genpv  9173  genpdm  9176  distrlem5pr  9201  mulid1  9388  ltne  9476  mul02  9552  cnegex  9555  mul0or  9981  sup2  10291  supmul1  10300  supmul  10303  creur  10321  creui  10322  cju  10323  nnsub  10365  un0addcl  10618  un0mulcl  10619  nn0sub  10635  elz2  10668  zaddcl  10690  suprzcl2  10950  qmulz  10961  qre  10963  qnegcl  10975  xrmax1  11152  xrmin2  11155  max1ALT  11163  xlesubadd  11231  xmulass  11255  xlemul1a  11256  xrsupexmnf  11272  xrinfmexpnf  11273  xrub  11279  iccid  11350  fzsn  11505  fzsuc2  11519  fz1sbc  11541  elfzp12  11544  fzm1  11545  seqid3  11855  bcval5  12099  bcpasc  12102  hashbnd  12114  hashnnn0genn0  12119  hashprg  12160  hashfzo  12195  wrdl1s1  12306  cats1un  12375  shftlem  12562  replim  12610  absmod0  12797  absz  12805  rlimdm  13034  summolem2  13198  summo  13199  zsum  13200  fsum  13202  fsummulc2  13256  fsumconst  13262  fsum00  13266  incexclem  13304  isumsplit  13308  infcvgaux1i  13324  ruclem2  13519  fzo0dvdseq  13591  bitsf1ocnv  13645  sadcaddlem  13658  smueqlem  13691  gcdabs1  13723  bezoutlem1  13727  bezoutlem3  13729  bezoutlem4  13730  dvdsgcd  13732  dvdsmulgcd  13743  dvdsprime  13781  coprm  13791  isprm5  13803  prmdvdsexpr  13807  rpexp  13811  phibndlem  13850  dfphi2  13854  odzdvds  13872  pythagtriplem1  13888  iserodd  13907  pceulem  13917  pcqmul  13925  pcqcl  13928  pcxcl  13932  pcneg  13945  pcabs  13946  pcgcd1  13948  pcz  13952  pcprmpw2  13953  pcprmpw  13954  pcaddlem  13955  pcadd  13956  pcmpt  13959  pockthg  13972  prmreclem5  13986  4sqlem4  14018  mul4sq  14020  vdwapun  14040  vdwlem2  14048  vdwlem6  14052  vdwlem8  14054  vdwlem13  14059  0ram  14086  ram0  14088  ramcl  14095  cshwsiun  14131  wunress  14242  firest  14376  xpscfv  14505  isssc  14738  pospo  15148  latnlej  15243  gsumval2a  15517  mulgnn0p1  15643  mulgnn0ass  15661  gicsubgen  15811  symg1bas  15906  psgnunilem1  16004  psgnunilem2  16006  mndodcongi  16051  oddvdsnn0  16052  odnncl  16053  oddvds  16055  odeq  16058  odeq1  16066  pgpfi2  16110  sylow2a  16123  sylow2blem3  16126  sylow3lem6  16136  lsmelvalm  16155  lsmsubm  16157  lsmsubg  16158  lsmmod  16177  lsmdisj2  16184  efgmnvl  16216  efgtlen  16228  efgs1b  16238  efgrelexlemb  16252  efgredeu  16254  efgcpbllemb  16257  frgpuptinv  16273  frgpup3lem  16279  divsabl  16352  frgpnabllem1  16356  cyggeninv  16365  cyggenod  16366  cygabl  16372  gsumval3eu  16386  dprdssv  16511  dprdfeq0  16517  dprdfeq0OLD  16524  dprdsubg  16526  dprddisj2  16542  dprddisj2OLD  16543  ablfacrp  16572  pgpfac1lem3  16583  pgpfaclem2  16588  dvreq1  16790  irredn1  16803  drngmul0or  16858  isabvd  16910  abvdom  16928  issrngd  16951  lss1d  17049  lspsneq0  17098  lbspss  17168  lsmcl  17169  lvecvs0or  17194  lspindpi  17218  lidl1el  17305  lpiss  17337  lidldvgen  17342  nzrunit  17353  rrgeq0  17366  domneq0  17374  mplsubrglem  17522  mplsubrglemOLD  17523  mplmonmul  17548  mplcoe5lem  17552  coe1tmmul2  17734  coe1tmmul  17735  pf1ind  17794  qsssubdrg  17877  zringlpirlem1  17908  zlpirlem1  17913  znfld  17998  znunit  18001  znrrg  18003  cygznlem3  18007  frgpcyg  18011  psgnghm  18015  ipeq0  18072  cssincl  18118  lsmcss  18122  obselocv  18158  dsmmacl  18171  dsmmlss  18174  mdetralt  18419  mdetunilem2  18424  mdetunilem7  18429  mdetunilem9  18431  maducoeval2  18451  istopon  18535  eltg3  18572  tgidm  18590  clsval2  18659  opncldf1  18693  restbas  18767  tgrest  18768  restcld  18781  restcldr  18783  restcls  18790  restntr  18791  ordtbas2  18800  ordtbas  18801  ordtrest2lem  18812  ordtrest2  18813  pnfnei  18829  mnfnei  18830  tgcn  18861  cnconst  18893  cnindis  18901  lmss  18907  ordtt1  18988  discmp  19006  1stcrest  19062  2ndcdisj  19065  cldllycmp  19104  txbas  19145  ptpjpre1  19149  ptuni2  19154  ptbasin  19155  ptbasfi  19159  ptopn2  19162  txbasval  19184  ptpjopn  19190  ptclsg  19193  dfac14lem  19195  xkoccn  19197  ptcnp  19200  upxp  19201  ptrescn  19217  txkgen  19230  xkoptsub  19232  xkopt  19233  xkoco1cn  19235  xkoco2cn  19236  xkococn  19238  xkoinjcn  19265  ordthmeolem  19379  ptuncnv  19385  nrmhaus  19404  fbssint  19416  fbfinnfr  19419  fbasrn  19462  isufil2  19486  filufint  19498  rnelfm  19531  fmfnfmlem2  19533  fmfnfmlem3  19534  fmfnfmlem4  19535  fmfnfm  19536  flimtopon  19548  flimclslem  19562  fclstopon  19590  fclscf  19603  flimfnfcls  19606  alexsublem  19621  alexsubALTlem3  19626  alexsubALTlem4  19627  ptcmplem2  19630  tmdgsum2  19672  symgtgp  19677  cldsubg  19686  divstgplem  19696  tgptsmscld  19730  tsmsxplem1  19732  imasdsf1olem  19953  blssps  20004  blss  20005  stdbdxmet  20095  methaus  20100  metrest  20104  nrginvrcn  20277  nmoeq0  20320  blssioo  20377  xrtgioo  20388  xrsxmet  20391  reconnlem1  20408  reconnlem2  20409  xrge0tsms  20416  elcncf1di  20476  iccpnfcnv  20521  evth  20536  lebnumlem1  20538  lebnumlem2  20539  lebnumlem3  20540  nmoleub3  20679  minveclem3b  20920  ivthlem2  20941  ivthlem3  20942  elovolm  20963  ovolmge0  20965  ovoliun  20993  ovolicc2lem3  21007  ovolicc2  21010  voliunlem3  21038  dyaddisj  21081  dyadmax  21083  opnmblALT  21088  ismbfd  21123  ismbf2d  21124  mbfimaopnlem  21138  mbfimaopn2  21140  i1fmullem  21177  i1fres  21188  itg1climres  21197  mbfi1fseqlem4  21201  itg2lcl  21210  itgsplitioo  21320  ellimc2  21357  rolle  21467  dvlip  21470  dvge0  21483  dvne0  21488  lhop1lem  21490  tdeglem4  21534  degltlem1  21548  deg1nn0clb  21566  deg1lt0  21567  dvdsq1p  21637  ply1rem  21640  fta1g  21644  elply2  21669  plyf  21671  ne0p  21680  plyeq0lem  21683  plypf1  21685  0dgrb  21719  coe1termlem  21730  dgrcolem2  21746  plymul0or  21752  plyrem  21776  fta1  21779  quotcan  21780  aalioulem3  21805  eff1olem  22009  lognegb  22043  eflogeq  22055  argregt0  22064  argrege0  22065  tanarg  22073  cxpexp  22118  cxpeq0  22128  mulcxp  22135  cxpeq  22200  atans2  22331  scvxcvx  22384  isppw2  22458  vmappw  22459  vmacl  22461  efvmacl  22463  isnsqf  22478  mumullem2  22523  sqff1o  22525  dvdsppwf1o  22531  ppiublem1  22546  vmalelog  22549  chtublem  22555  fsumvma  22557  perfectlem2  22574  perfect  22575  bposlem1  22628  lgsmod  22665  lgsne0  22677  lgsdirnn0  22683  lgsqr  22690  lgsdchr  22692  lgseisenlem2  22694  lgsquadlem1  22698  lgsquadlem2  22699  2sqlem2  22708  mul2sq  22709  2sqlem7  22714  dchrisum0fno1  22765  pntrsumbnd2  22821  ostthlem1  22881  ostth2lem2  22888  ostth3  22892  ostth  22893  colinearalg  23161  axpasch  23192  axlowdimlem16  23208  axlowdimlem17  23209  axlowdim  23212  axcontlem2  23216  axcontlem4  23218  axcontlem7  23221  usgraexmpl  23324  nbgraf1olem1  23355  nbgraf1olem3  23357  nbgraf1olem5  23359  nb3graprlem2  23365  cusgrasize2inds  23390  vdgr1a  23581  vdusgra0nedg  23583  usgravd0nedg  23587  eupap1  23602  ismndo2  23837  ghgrplem1  23858  rngosn4  23919  nvmul0or  24037  ipasslem5  24240  ipasslem11  24245  hvmul0or  24432  his6  24506  hhssnv  24670  ocsh  24691  ocin  24704  shsidmi  24792  chnlen0  24852  h1de2bi  24962  h1de2ctlem  24963  h1de2ci  24964  spansni  24965  3oalem1  25070  nmcexi  25435  atcveq0  25757  chcv1  25764  cdjreui  25841  cdj3lem2b  25846  xrge0tsmsd  26258  ordtrest2NEWlem  26357  ordtrest2NEW  26358  xrge0iifcnv  26368  esumc  26510  esumpcvgval  26532  ballotlemfc0  26880  ballotlemfcc  26881  dmgmaddn0  27014  subfacp1lem4  27076  subfacp1lem5  27077  erdszelem8  27091  sconpi1  27133  cvmsss2  27168  cvmlift2lem12  27208  sinccvglem  27322  untsucf  27366  prodmolem2  27453  prodmo  27454  zprod  27455  fprod  27459  prodsn  27478  fprodconst  27494  dfpo2  27570  dfrdg2  27614  trpred0  27705  wfrlem10  27738  wfrlem14  27742  wfrlem15  27743  frrlem4  27776  colineardim1  28097  btwnconn1lem14  28136  segleantisym  28151  colinbtwnle  28154  outsidele  28168  lineunray  28183  linethru  28189  supaddc  28422  supadd  28423  itg2addnclem3  28450  ftc1anclem6  28477  dvasin  28485  elicc3  28517  opnregcld  28530  cldregopn  28531  fnejoin2  28595  unirep  28611  sdclem2  28643  ssbnd  28692  prdsbnd  28697  cntotbnd  28700  heibor1lem  28713  rrnequiv  28739  grpoeqdivid  28751  isdrngo3  28770  crngohomfo  28811  0idl  28830  1idl  28831  divrngidl  28833  smprngopr  28857  prnc  28872  ispridlc  28875  elrfi  29035  mrefg2  29048  eldiophb  29100  eldioph2b  29106  diophin  29116  diophun  29117  rexzrexnn0  29147  eldioph4b  29155  diophren  29157  rencldnfilem  29164  pellexlem6  29180  jm2.19  29347  rmydioph  29368  expdiophlem1  29375  expdioph  29377  lnr2i  29477  lpirlnr  29478  hbtlem2  29485  hbtlem4  29487  hbtlem6  29490  dgrsub2  29496  dgraa0p  29511  rngunsnply  29535  hashgcdlem  29570  pm14.24  29691  addrcom  29736  afveu  30064  dfafn5b  30072  rlimdmafv  30088  wlklenfislenpm1  30289  wlklniswwlkn2  30339  wlkiswwlksur  30356  wwlknextbi  30362  clwlkisclwwlklem1  30454  clwwisshclww  30476  erclwwlktr  30490  erclwwlkntr  30506  clwlkfclwwlk1hash  30520  0eusgraiff0rgra  30557  rusgraprop2  30559  wwlkextproplem2  30566  vdn0frgrav2  30621  vdgn0frgrav2  30622  fmptsnd  30727  mpt2sn  30728  mat1dimelbas  30872  lincellss  30965  lindsrng01  31007  bnj145OLD  31723  riotaclbgBAD  32610  riotaclbBAD  32611  lshpdisj  32637  lsateln0  32645  lsatcveq0  32682  opnlen0  32838  cmtbr4N  32905  cvrnbtwn2  32925  cvrnbtwn4  32929  atcvreq0  32964  cvlatexch1  32986  exatleN  33053  atlelt  33087  ps-2  33127  llnn0  33165  lplnn0N  33196  islpln2a  33197  lvoln0N  33240  islvol2aN  33241  4at  33262  dalemcea  33309  dalem3  33313  pmapglb2N  33420  pmapglb2xN  33421  cdlema1N  33440  cdlemb  33443  paddasslem17  33485  llnexchb2lem  33517  llnexchb2  33518  lhpat3  33695  ltrnid  33784  trlne  33834  cdlemc4  33843  cdleme11h  33915  cdlemednuN  33949  cdlemg1a  34219  tendoeq2  34423  tendoid0  34474  dva1dim  34634  dib1dim  34815  dihlatat  34987  dochkrshp4  35039  dochkr1  35128  lclkrlem2e  35161  lcfrlem16  35208  lcfrlem28  35220  mapd0  35315  hdmap14lem13  35533
  Copyright terms: Public domain W3C validator