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  2022  elsnc2g  3670  opth1  4246  euotd  4269  tz7.2  4379  ordtri1  4427  reusv2lem2  4538  reusv3  4544  alxfr  4549  reuhypd  4563  oneqmin  4598  nlimsucg  4635  onzsl  4639  tfinds  4652  xpsspw  4799  funcnvuni  5319  fvmptdv2  5615  foco2  5682  fsn  5698  fconst2g  5730  funfvima  5755  soisoi  5827  isores3  5834  ovmpt2dv2  5983  f1opw2  6073  suppssfv  6076  suppssov1  6077  brtpos  6245  sorpssun  6286  sorpssin  6287  opiota  6292  eusvobj2  6339  riotaclbg  6346  seqomlem1  6464  seqomlem2  6465  omordi  6566  omord  6568  omwordi  6571  oeeui  6602  nnmordi  6631  nnmord  6632  nnmwordi  6635  nnawordex  6637  nnaordex  6638  nneob  6652  omsmolem  6653  qsss  6722  eroveu  6755  th3qlem1  6766  mapsncnv  6816  elixpsn  6857  ixpsnf1o  6858  boxcutc  6861  pw2f1olem  6968  2pwne  7019  mapxpen  7029  mapunen  7032  php  7047  unxpdomlem2  7070  isfiniteg  7119  fofinf1o  7139  f1opwfi  7161  elfiun  7185  oieu  7256  brwdom2  7289  wdomtr  7291  ixpiunwdom  7307  suc11reg  7322  inf3lemd  7330  cantnfvalf  7368  cantnflt  7375  cantnfp1lem3  7384  cantnflem2  7394  en3lplem1  7418  r1tr  7450  dfac8alem  7658  wdomnumr  7693  isinfcard  7721  aceq3lem  7749  dfac5lem4  7755  dfac5  7757  dfac2  7759  coftr  7901  fin23lem28  7968  fin23lem29  7969  fin1a2lem11  8038  fin1a2lem12  8039  fin1a2lem13  8040  hsmexlem9  8053  axdclem  8148  pwcfsdom  8207  gchdomtri  8253  fpwwe2  8267  gchhar  8295  gchpwdom  8298  addnidpi  8527  nqereu  8555  genpv  8625  genpdm  8628  distrlem5pr  8653  mulid1  8837  ltne  8919  mul02  8992  cnegex  8995  mul0or  9410  sup2  9712  supmul1  9721  supmul  9724  creur  9742  creui  9743  cju  9744  nnsub  9786  un0addcl  9999  un0mulcl  10000  nn0sub  10016  elz2  10042  zaddcl  10061  suprzcl2  10310  qmulz  10321  qre  10323  qnegcl  10335  xrmax1  10506  xrmin2  10509  max1ALT  10517  xlesubadd  10585  xmulass  10609  xlemul1a  10610  xrsupexmnf  10625  xrinfmexpnf  10626  xrub  10632  iccid  10703  fzsn  10835  fzsuc2  10844  fz1sbc  10861  elfzp12  10863  fzm1  10864  seqid3  11092  bcval5  11332  bcpasc  11335  hashbnd  11345  hashprg  11370  hashfzo  11385  cats1un  11478  shftlem  11565  replim  11603  absmod0  11790  absz  11798  rlimdm  12027  summolem2  12191  summo  12192  zsum  12193  fsum  12195  fsummulc2  12248  fsumconst  12254  fsum00  12258  incexclem  12297  isumsplit  12301  infcvgaux1i  12317  ruclem2  12512  fzo0dvdseq  12583  bitsf1ocnv  12637  sadcaddlem  12650  smueqlem  12683  gcdabs1  12715  bezoutlem1  12719  bezoutlem3  12721  bezoutlem4  12722  dvdsgcd  12724  dvdsmulgcd  12735  dvdsprime  12773  coprm  12781  isprm5  12793  prmdvdsexpr  12797  rpexp  12801  phibndlem  12840  dfphi2  12844  odzdvds  12862  pythagtriplem1  12871  iserodd  12890  pceulem  12900  pcqmul  12908  pcqcl  12911  pcxcl  12915  pcneg  12928  pcabs  12929  pcgcd1  12931  pcz  12935  pcprmpw2  12936  pcprmpw  12937  pcaddlem  12938  pcadd  12939  pcmpt  12942  pockthg  12955  prmreclem5  12969  4sqlem4  13001  mul4sq  13003  vdwapun  13023  vdwlem2  13031  vdwlem6  13035  vdwlem8  13037  vdwlem13  13042  0ram  13069  ram0  13071  ramcl  13078  wunress  13209  firest  13339  xpscfv  13466  isssc  13699  pospo  14109  latnlej  14176  gsumval2a  14461  mulgnn0p1  14580  mulgnn0ass  14598  gicsubgen  14744  mndodcongi  14860  oddvdsnn0  14861  odnncl  14862  oddvds  14864  odeq  14867  odeq1  14875  pgpfi2  14919  sylow2a  14932  sylow2blem3  14935  sylow3lem6  14945  lsmelvalm  14964  lsmsubm  14966  lsmsubg  14967  lsmmod  14986  lsmdisj2  14993  efgmnvl  15025  efgtlen  15037  efgs1b  15047  efgrelexlemb  15061  efgredeu  15063  efgcpbllemb  15066  frgpuptinv  15082  frgpup3lem  15088  divsabl  15159  frgpnabllem1  15163  cyggeninv  15172  cyggenod  15173  cygabl  15179  gsumval3eu  15192  dprdssv  15253  dprdfeq0  15259  dprdsubg  15261  dprddisj2  15276  ablfacrp  15303  pgpfac1lem3  15314  pgpfaclem2  15319  dvreq1  15477  irredn1  15490  drngmul0or  15535  isabvd  15587  abvdom  15605  issrngd  15628  lss1d  15722  lspsneq0  15771  lbspss  15837  lsmcl  15838  lvecvs0or  15863  lspindpi  15887  lidl1el  15972  lpiss  16004  lidldvgen  16009  nzrunit  16020  rrgeq0  16033  domneq0  16040  mplsubrglem  16185  mplmonmul  16210  coe1tmmul2  16354  coe1tmmul  16355  qsssubdrg  16433  zlpirlem1  16443  znfld  16516  znunit  16519  znrrg  16521  cygznlem3  16525  frgpcyg  16529  ipeq0  16544  cssincl  16590  lsmcss  16594  obselocv  16630  istopon  16665  eltg3  16702  tgidm  16720  clsval2  16789  opncldf1  16823  restbas  16891  tgrest  16892  restcld  16905  restcldr  16907  restcls  16913  restntr  16914  ordtbas2  16923  ordtbas  16924  ordtrest2lem  16935  ordtrest2  16936  pnfnei  16952  mnfnei  16953  tgcn  16984  cnconst  17014  cnindis  17022  lmss  17028  ordtt1  17109  discmp  17127  1stcrest  17181  2ndcdisj  17184  cldllycmp  17223  txbas  17264  ptpjpre1  17268  ptuni2  17273  ptbasin  17274  ptbasfi  17278  ptopn2  17281  txbasval  17303  ptpjopn  17308  ptclsg  17311  dfac14lem  17313  xkoccn  17315  ptcnp  17318  upxp  17319  ptrescn  17335  txkgen  17348  xkoptsub  17350  xkopt  17351  xkoco1cn  17353  xkoco2cn  17354  xkococn  17356  xkoinjcn  17383  ordthmeolem  17494  ptuncnv  17500  nrmhaus  17519  fbssint  17535  fbfinnfr  17538  fbasrn  17581  isufil2  17605  filufint  17617  rnelfm  17650  fmfnfmlem2  17652  fmfnfmlem3  17653  fmfnfmlem4  17654  fmfnfm  17655  flimtopon  17667  flimclslem  17681  fclstopon  17709  fclscf  17722  flimfnfcls  17725  alexsublem  17740  alexsubALTlem3  17745  alexsubALTlem4  17746  ptcmplem2  17749  tmdgsum2  17781  symgtgp  17786  cldsubg  17795  divstgplem  17805  tgptsmscld  17835  tsmsxplem1  17837  imasdsf1olem  17939  blss  17974  stdbdxmet  18063  methaus  18068  metrest  18072  nrginvrcn  18204  nmoeq0  18247  blssioo  18303  xrtgioo  18314  xrsxmet  18317  reconnlem1  18333  reconnlem2  18334  xrge0tsms  18341  elcncf1di  18401  iccpnfcnv  18444  evth  18459  lebnumlem1  18461  lebnumlem2  18462  lebnumlem3  18463  nmoleub3  18602  minveclem3b  18794  ivthlem2  18814  ivthlem3  18815  elovolm  18836  ovolmge0  18838  ovoliun  18866  ovolicc2lem3  18880  ovolicc2  18883  voliunlem3  18911  dyaddisj  18953  dyadmax  18955  opnmblALT  18960  ismbfd  18997  ismbf2d  18998  mbfimaopnlem  19012  mbfimaopn2  19014  i1fmullem  19051  i1fres  19062  itg1climres  19071  mbfi1fseqlem4  19075  itg2lcl  19084  itgsplitioo  19194  ellimc2  19229  rolle  19339  dvlip  19342  dvge0  19355  dvne0  19360  lhop1lem  19362  pf1ind  19440  tdeglem4  19448  degltlem1  19460  deg1nn0clb  19478  deg1lt0  19479  dvdsq1p  19548  ply1rem  19551  fta1g  19555  elply2  19580  plyf  19582  ne0p  19591  plyeq0lem  19594  plypf1  19596  0dgrb  19630  coe1termlem  19641  dgrcolem2  19657  plymul0or  19663  plyrem  19687  fta1  19690  quotcan  19691  aalioulem3  19716  eff1olem  19912  lognegb  19945  eflogeq  19957  argregt0  19966  argrege0  19967  tanarg  19972  cxpexp  20017  cxpeq0  20027  mulcxp  20034  cxpeq  20099  atans2  20229  scvxcvx  20282  isppw2  20355  vmappw  20356  vmacl  20358  efvmacl  20360  isnsqf  20375  mumullem2  20420  sqff1o  20422  dvdsppwf1o  20428  ppiublem1  20443  vmalelog  20446  chtublem  20452  fsumvma  20454  perfectlem2  20471  perfect  20472  bposlem1  20525  lgsmod  20562  lgsne0  20574  lgsdirnn0  20580  lgsqr  20587  lgsdchr  20589  lgseisenlem2  20591  lgsquadlem1  20595  lgsquadlem2  20596  2sqlem2  20605  mul2sq  20606  2sqlem7  20611  dchrisum0fno1  20662  pntrsumbnd2  20718  ostthlem1  20778  ostth2lem2  20785  ostth3  20789  ostth  20790  ismndo2  21014  ghgrplem1  21035  rngosn4  21096  nvmul0or  21212  ipasslem5  21415  ipasslem11  21420  hvmul0or  21606  his6  21680  hhssnv  21843  ocsh  21864  ocin  21877  shsidmi  21965  chnlen0  22025  h1de2bi  22135  h1de2ctlem  22136  h1de2ci  22137  spansni  22138  3oalem1  22243  nmcexi  22608  atcveq0  22930  chcv1  22937  cdjreui  23014  cdj3lem2b  23019  ballotlemfc0  23053  ballotlemfcc  23054  xrge0iifcnv  23317  xrge0tsmsd  23384  esumc  23432  esumpcvgval  23448  dmgmaddn0  23697  subfacp1lem4  23716  subfacp1lem5  23717  erdszelem8  23731  sconpi1  23772  cvmsss2  23807  cvmlift2lem12  23847  vdgr1a  23899  eupap1  23902  sinccvglem  24007  untsucf  24058  dfpo2  24114  dfrdg2  24154  trpred0  24241  wfrlem14  24271  wfrlem15  24272  frrlem4  24286  funpartfv  24485  colinearalg  24540  axpasch  24571  axlowdimlem16  24587  axlowdimlem17  24588  axlowdim  24591  axcontlem2  24595  axcontlem4  24597  axcontlem7  24600  colineardim1  24686  btwnconn1lem14  24725  segleantisym  24740  colinbtwnle  24743  outsidele  24757  lineunray  24772  linethru  24778  supaddc  24927  supadd  24928  repfuntw  25171  repcpwti  25172  cbicp  25177  trran2  25404  ltrran2  25414  rltrran  25425  intfmu2  25530  cldifemp  25535  efilcp  25563  islimrs3  25592  trran  25625  addcanri  25677  intvconlem1  25714  vtarsuelt  25906  partarelt1  25907  clscnc  26021  elicc3  26239  opnregcld  26259  cldregopn  26260  fnejoin2  26329  unirep  26360  sdclem2  26463  ssbnd  26523  prdsbnd  26528  cntotbnd  26531  heibor1lem  26544  rrnequiv  26570  grpoeqdivid  26582  isdrngo3  26601  crngohomfo  26642  0idl  26661  1idl  26662  divrngidl  26664  smprngopr  26688  prnc  26703  ispridlc  26706  ralxpmap  26772  elrfi  26780  mrefg2  26793  eldiophb  26847  eldioph2b  26853  diophin  26863  diophun  26864  rexzrexnn0  26896  eldioph4b  26905  diophren  26907  rencldnfilem  26914  pellexlem6  26930  jm2.19  27097  rmydioph  27118  expdiophlem1  27125  expdioph  27127  dsmmacl  27218  dsmmlss  27221  lnr2i  27331  lpirlnr  27332  hbtlem2  27339  hbtlem4  27341  hbtlem6  27344  dgrsub2  27350  dgraa0p  27365  rngunsnply  27389  psgnunilem1  27427  psgnunilem2  27429  psgnghm  27448  hashgcdlem  27527  pm14.24  27643  addrcom  27691  dfafn5b  28034  bnj145  28828  lshpdisj  29250  lsateln0  29258  lsatcveq0  29295  opnlen0  29451  glb0N  29456  cmtbr4N  29518  cvrnbtwn2  29538  cvrnbtwn4  29542  atcvreq0  29577  cvlatexch1  29599  exatleN  29666  atlelt  29700  ps-2  29740  llnn0  29778  lplnn0N  29809  islpln2a  29810  lvoln0N  29853  islvol2aN  29854  4at  29875  dalemcea  29922  dalem3  29926  pmapglb2N  30033  pmapglb2xN  30034  cdlema1N  30053  cdlemb  30056  paddasslem17  30098  llnexchb2lem  30130  llnexchb2  30131  lhpat3  30308  ltrnid  30397  trlne  30447  cdlemc4  30456  cdleme11h  30528  cdlemednuN  30562  cdlemg1a  30832  tendoeq2  31036  tendoid0  31087  dva1dim  31247  dib1dim  31428  dihlatat  31600  dochkrshp4  31652  dochkr1  31741  lclkrlem2e  31774  lcfrlem16  31821  lcfrlem28  31833  mapd0  31928  hdmap14lem13  32146
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