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  2085  elsnc2g  3744  opth1  4323  euotd  4346  tz7.2  4456  ordtri1  4504  reusv2lem2  4615  reusv3  4621  alxfr  4626  reuhypd  4640  oneqmin  4675  nlimsucg  4712  onzsl  4716  tfinds  4729  xpsspw  4876  funcnvuni  5396  fvmptdv2  5693  foco2  5760  fsn  5776  fconst2g  5809  fnpr  5813  fnprOLD  5814  funfvima  5836  soisoi  5909  isores3  5916  ovmpt2dv2  6065  f1opw2  6155  suppssfv  6158  suppssov1  6159  brtpos  6327  sorpssun  6368  sorpssin  6369  opiota  6374  eusvobj2  6421  riotaclbg  6428  seqomlem1  6546  seqomlem2  6547  omordi  6648  omord  6650  omwordi  6653  oeeui  6684  nnmordi  6713  nnmord  6714  nnmwordi  6717  nnawordex  6719  nnaordex  6720  nneob  6734  omsmolem  6735  qsss  6804  eroveu  6838  th3qlem1  6849  mapsncnv  6899  elixpsn  6940  ixpsnf1o  6941  boxcutc  6944  pw2f1olem  7051  2pwne  7102  mapxpen  7112  mapunen  7115  php  7130  unxpdomlem2  7153  isfiniteg  7204  fofinf1o  7224  f1opwfi  7246  elfiun  7270  oieu  7341  brwdom2  7374  wdomtr  7376  ixpiunwdom  7392  suc11reg  7407  inf3lemd  7415  cantnfvalf  7453  cantnflt  7460  cantnfp1lem3  7469  cantnflem2  7479  en3lplem1  7503  r1tr  7535  dfac8alem  7743  wdomnumr  7778  isinfcard  7806  aceq3lem  7834  dfac5lem4  7840  dfac5  7842  dfac2  7844  coftr  7986  fin23lem28  8053  fin23lem29  8054  fin1a2lem11  8123  fin1a2lem12  8124  fin1a2lem13  8125  hsmexlem9  8138  axdclem  8233  pwcfsdom  8292  gchdomtri  8338  fpwwe2  8352  gchhar  8380  gchpwdom  8383  addnidpi  8612  nqereu  8640  genpv  8710  genpdm  8713  distrlem5pr  8738  mulid1  8922  ltne  9004  mul02  9077  cnegex  9080  mul0or  9495  sup2  9797  supmul1  9806  supmul  9809  creur  9827  creui  9828  cju  9829  nnsub  9871  un0addcl  10086  un0mulcl  10087  nn0sub  10103  elz2  10129  zaddcl  10148  suprzcl2  10397  qmulz  10408  qre  10410  qnegcl  10422  xrmax1  10593  xrmin2  10596  max1ALT  10604  xlesubadd  10672  xmulass  10696  xlemul1a  10697  xrsupexmnf  10712  xrinfmexpnf  10713  xrub  10719  iccid  10790  fzsn  10922  fzsuc2  10931  fz1sbc  10948  elfzp12  10950  fzm1  10951  seqid3  11179  bcval5  11420  bcpasc  11423  hashbnd  11433  hashprg  11458  hashfzo  11473  cats1un  11566  shftlem  11653  replim  11691  absmod0  11878  absz  11886  rlimdm  12115  summolem2  12280  summo  12281  zsum  12282  fsum  12284  fsummulc2  12337  fsumconst  12343  fsum00  12347  incexclem  12386  isumsplit  12390  infcvgaux1i  12406  ruclem2  12601  fzo0dvdseq  12672  bitsf1ocnv  12726  sadcaddlem  12739  smueqlem  12772  gcdabs1  12804  bezoutlem1  12808  bezoutlem3  12810  bezoutlem4  12811  dvdsgcd  12813  dvdsmulgcd  12824  dvdsprime  12862  coprm  12870  isprm5  12882  prmdvdsexpr  12886  rpexp  12890  phibndlem  12929  dfphi2  12933  odzdvds  12951  pythagtriplem1  12960  iserodd  12979  pceulem  12989  pcqmul  12997  pcqcl  13000  pcxcl  13004  pcneg  13017  pcabs  13018  pcgcd1  13020  pcz  13024  pcprmpw2  13025  pcprmpw  13026  pcaddlem  13027  pcadd  13028  pcmpt  13031  pockthg  13044  prmreclem5  13058  4sqlem4  13090  mul4sq  13092  vdwapun  13112  vdwlem2  13120  vdwlem6  13124  vdwlem8  13126  vdwlem13  13131  0ram  13158  ram0  13160  ramcl  13167  wunress  13298  firest  13430  xpscfv  13557  isssc  13790  pospo  14200  latnlej  14267  gsumval2a  14552  mulgnn0p1  14671  mulgnn0ass  14689  gicsubgen  14835  mndodcongi  14951  oddvdsnn0  14952  odnncl  14953  oddvds  14955  odeq  14958  odeq1  14966  pgpfi2  15010  sylow2a  15023  sylow2blem3  15026  sylow3lem6  15036  lsmelvalm  15055  lsmsubm  15057  lsmsubg  15058  lsmmod  15077  lsmdisj2  15084  efgmnvl  15116  efgtlen  15128  efgs1b  15138  efgrelexlemb  15152  efgredeu  15154  efgcpbllemb  15157  frgpuptinv  15173  frgpup3lem  15179  divsabl  15250  frgpnabllem1  15254  cyggeninv  15263  cyggenod  15264  cygabl  15270  gsumval3eu  15283  dprdssv  15344  dprdfeq0  15350  dprdsubg  15352  dprddisj2  15367  ablfacrp  15394  pgpfac1lem3  15405  pgpfaclem2  15410  dvreq1  15568  irredn1  15581  drngmul0or  15626  isabvd  15678  abvdom  15696  issrngd  15719  lss1d  15813  lspsneq0  15862  lbspss  15928  lsmcl  15929  lvecvs0or  15954  lspindpi  15978  lidl1el  16063  lpiss  16095  lidldvgen  16100  nzrunit  16111  rrgeq0  16124  domneq0  16131  mplsubrglem  16276  mplmonmul  16301  coe1tmmul2  16445  coe1tmmul  16446  qsssubdrg  16531  zlpirlem1  16541  znfld  16614  znunit  16617  znrrg  16619  cygznlem3  16623  frgpcyg  16627  ipeq0  16642  cssincl  16688  lsmcss  16692  obselocv  16728  istopon  16763  eltg3  16800  tgidm  16818  clsval2  16887  opncldf1  16921  restbas  16989  tgrest  16990  restcld  17003  restcldr  17005  restcls  17011  restntr  17012  ordtbas2  17021  ordtbas  17022  ordtrest2lem  17033  ordtrest2  17034  pnfnei  17050  mnfnei  17051  tgcn  17082  cnconst  17112  cnindis  17120  lmss  17126  ordtt1  17207  discmp  17225  1stcrest  17279  2ndcdisj  17282  cldllycmp  17321  txbas  17362  ptpjpre1  17366  ptuni2  17371  ptbasin  17372  ptbasfi  17376  ptopn2  17379  txbasval  17401  ptpjopn  17406  ptclsg  17409  dfac14lem  17411  xkoccn  17413  ptcnp  17416  upxp  17417  ptrescn  17433  txkgen  17446  xkoptsub  17448  xkopt  17449  xkoco1cn  17451  xkoco2cn  17452  xkococn  17454  xkoinjcn  17481  ordthmeolem  17592  ptuncnv  17598  nrmhaus  17617  fbssint  17629  fbfinnfr  17632  fbasrn  17675  isufil2  17699  filufint  17711  rnelfm  17744  fmfnfmlem2  17746  fmfnfmlem3  17747  fmfnfmlem4  17748  fmfnfm  17749  flimtopon  17761  flimclslem  17775  fclstopon  17803  fclscf  17816  flimfnfcls  17819  alexsublem  17834  alexsubALTlem3  17839  alexsubALTlem4  17840  ptcmplem2  17843  tmdgsum2  17875  symgtgp  17880  cldsubg  17889  divstgplem  17899  tgptsmscld  17929  tsmsxplem1  17931  imasdsf1olem  18033  blss  18068  stdbdxmet  18157  methaus  18162  metrest  18166  nrginvrcn  18298  nmoeq0  18341  blssioo  18397  xrtgioo  18408  xrsxmet  18411  reconnlem1  18428  reconnlem2  18429  xrge0tsms  18436  elcncf1di  18496  iccpnfcnv  18540  evth  18555  lebnumlem1  18557  lebnumlem2  18558  lebnumlem3  18559  nmoleub3  18698  minveclem3b  18890  ivthlem2  18910  ivthlem3  18911  elovolm  18932  ovolmge0  18934  ovoliun  18962  ovolicc2lem3  18976  ovolicc2  18979  voliunlem3  19007  dyaddisj  19049  dyadmax  19051  opnmblALT  19056  ismbfd  19093  ismbf2d  19094  mbfimaopnlem  19108  mbfimaopn2  19110  i1fmullem  19147  i1fres  19158  itg1climres  19167  mbfi1fseqlem4  19171  itg2lcl  19180  itgsplitioo  19290  ellimc2  19325  rolle  19435  dvlip  19438  dvge0  19451  dvne0  19456  lhop1lem  19458  pf1ind  19536  tdeglem4  19544  degltlem1  19556  deg1nn0clb  19574  deg1lt0  19575  dvdsq1p  19644  ply1rem  19647  fta1g  19651  elply2  19676  plyf  19678  ne0p  19687  plyeq0lem  19690  plypf1  19692  0dgrb  19726  coe1termlem  19737  dgrcolem2  19753  plymul0or  19759  plyrem  19783  fta1  19786  quotcan  19787  aalioulem3  19812  eff1olem  20011  lognegb  20045  eflogeq  20057  argregt0  20066  argrege0  20067  tanarg  20075  cxpexp  20120  cxpeq0  20130  mulcxp  20137  cxpeq  20202  atans2  20332  scvxcvx  20385  isppw2  20459  vmappw  20460  vmacl  20462  efvmacl  20464  isnsqf  20479  mumullem2  20524  sqff1o  20526  dvdsppwf1o  20532  ppiublem1  20547  vmalelog  20550  chtublem  20556  fsumvma  20558  perfectlem2  20575  perfect  20576  bposlem1  20629  lgsmod  20666  lgsne0  20678  lgsdirnn0  20684  lgsqr  20691  lgsdchr  20693  lgseisenlem2  20695  lgsquadlem1  20699  lgsquadlem2  20700  2sqlem2  20709  mul2sq  20710  2sqlem7  20715  dchrisum0fno1  20766  pntrsumbnd2  20822  ostthlem1  20882  ostth2lem2  20889  ostth3  20893  ostth  20894  ismndo2  21118  ghgrplem1  21139  rngosn4  21200  nvmul0or  21318  ipasslem5  21521  ipasslem11  21526  hvmul0or  21712  his6  21786  hhssnv  21949  ocsh  21970  ocin  21983  shsidmi  22071  chnlen0  22131  h1de2bi  22241  h1de2ctlem  22242  h1de2ci  22243  spansni  22244  3oalem1  22349  nmcexi  22714  atcveq0  23036  chcv1  23043  cdjreui  23120  cdj3lem2b  23125  xrge0tsmsd  23415  xrge0iifcnv  23475  esumc  23712  esumpcvgval  23734  ballotlemfc0  23999  ballotlemfcc  24000  dmgmaddn0  24056  subfacp1lem4  24118  subfacp1lem5  24119  erdszelem8  24133  sconpi1  24174  cvmsss2  24209  cvmlift2lem12  24249  vdgr1a  24301  eupap1  24304  sinccvglem  24409  untsucf  24460  prodmolem2  24562  prodmo  24563  zprod  24564  fprod  24568  prodsn  24587  fprodconst  24603  dfpo2  24670  dfrdg2  24710  trpred0  24797  wfrlem14  24827  wfrlem15  24828  frrlem4  24842  colinearalg  25097  axpasch  25128  axlowdimlem16  25144  axlowdimlem17  25145  axlowdim  25148  axcontlem2  25152  axcontlem4  25154  axcontlem7  25157  colineardim1  25243  btwnconn1lem14  25282  segleantisym  25297  colinbtwnle  25300  outsidele  25314  lineunray  25329  linethru  25335  supaddc  25482  supadd  25483  elicc3  25552  opnregcld  25572  cldregopn  25573  fnejoin2  25642  unirep  25673  sdclem2  25776  ssbnd  25835  prdsbnd  25840  cntotbnd  25843  heibor1lem  25856  rrnequiv  25882  grpoeqdivid  25894  isdrngo3  25913  crngohomfo  25954  0idl  25973  1idl  25974  divrngidl  25976  smprngopr  26000  prnc  26015  ispridlc  26018  ralxpmap  26084  elrfi  26092  mrefg2  26105  eldiophb  26159  eldioph2b  26165  diophin  26175  diophun  26176  rexzrexnn0  26208  eldioph4b  26217  diophren  26219  rencldnfilem  26226  pellexlem6  26242  jm2.19  26409  rmydioph  26430  expdiophlem1  26437  expdioph  26439  dsmmacl  26530  dsmmlss  26533  lnr2i  26643  lpirlnr  26644  hbtlem2  26651  hbtlem4  26653  hbtlem6  26656  dgrsub2  26662  dgraa0p  26677  rngunsnply  26701  psgnunilem1  26739  psgnunilem2  26741  psgnghm  26760  hashgcdlem  26839  pm14.24  26955  addrcom  27003  afveu  27341  dfafn5b  27349  rlimdmafv  27365  hashnnn0genn0  27472  nbgraf1olem1  27597  nbgraf1olem3  27599  nbgraf1olem5  27601  nb3graprlem2  27607  cusgrasize2inds  27632  vdgre1a  27796  vdusgra0nedg  27799  usgravd0nedg  27803  vdn0frgrav2  27840  vdgn0frgrav2  27841  bnj145  28500  nfsb4twAUX7  28980  nfsb4tOLD7  29129  nfsb4tw2AUXOLD7  29130  lshpdisj  29229  lsateln0  29237  lsatcveq0  29274  opnlen0  29430  glb0N  29435  cmtbr4N  29497  cvrnbtwn2  29517  cvrnbtwn4  29521  atcvreq0  29556  cvlatexch1  29578  exatleN  29645  atlelt  29679  ps-2  29719  llnn0  29757  lplnn0N  29788  islpln2a  29789  lvoln0N  29832  islvol2aN  29833  4at  29854  dalemcea  29901  dalem3  29905  pmapglb2N  30012  pmapglb2xN  30013  cdlema1N  30032  cdlemb  30035  paddasslem17  30077  llnexchb2lem  30109  llnexchb2  30110  lhpat3  30287  ltrnid  30376  trlne  30426  cdlemc4  30435  cdleme11h  30507  cdlemednuN  30541  cdlemg1a  30811  tendoeq2  31015  tendoid0  31066  dva1dim  31226  dib1dim  31407  dihlatat  31579  dochkrshp4  31631  dochkr1  31720  lclkrlem2e  31753  lcfrlem16  31800  lcfrlem28  31812  mapd0  31907  hdmap14lem13  32125
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