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  4326  euotd  4349  tz7.2  4459  ordtri1  4507  reusv2lem2  4618  reusv3  4624  alxfr  4629  reuhypd  4643  oneqmin  4678  nlimsucg  4715  onzsl  4719  tfinds  4732  xpsspw  4879  funcnvuni  5399  fvmptdv2  5696  foco2  5763  fsn  5779  fconst2g  5812  fnpr  5816  fnprOLD  5817  funfvima  5839  soisoi  5912  isores3  5919  ovmpt2dv2  6068  f1opw2  6158  suppssfv  6161  suppssov1  6162  brtpos  6330  sorpssun  6371  sorpssin  6372  opiota  6377  eusvobj2  6424  riotaclbg  6431  seqomlem1  6549  seqomlem2  6550  omordi  6651  omord  6653  omwordi  6656  oeeui  6687  nnmordi  6716  nnmord  6717  nnmwordi  6720  nnawordex  6722  nnaordex  6723  nneob  6737  omsmolem  6738  qsss  6807  eroveu  6841  th3qlem1  6852  mapsncnv  6902  elixpsn  6943  ixpsnf1o  6944  boxcutc  6947  pw2f1olem  7054  2pwne  7105  mapxpen  7115  mapunen  7118  php  7133  unxpdomlem2  7156  isfiniteg  7207  fofinf1o  7227  f1opwfi  7249  elfiun  7273  oieu  7344  brwdom2  7377  wdomtr  7379  ixpiunwdom  7395  suc11reg  7410  inf3lemd  7418  cantnfvalf  7456  cantnflt  7463  cantnfp1lem3  7472  cantnflem2  7482  en3lplem1  7506  r1tr  7538  dfac8alem  7746  wdomnumr  7781  isinfcard  7809  aceq3lem  7837  dfac5lem4  7843  dfac5  7845  dfac2  7847  coftr  7989  fin23lem28  8056  fin23lem29  8057  fin1a2lem11  8126  fin1a2lem12  8127  fin1a2lem13  8128  hsmexlem9  8141  axdclem  8236  pwcfsdom  8295  gchdomtri  8341  fpwwe2  8355  gchhar  8383  gchpwdom  8386  addnidpi  8615  nqereu  8643  genpv  8713  genpdm  8716  distrlem5pr  8741  mulid1  8925  ltne  9007  mul02  9080  cnegex  9083  mul0or  9498  sup2  9800  supmul1  9809  supmul  9812  creur  9830  creui  9831  cju  9832  nnsub  9874  un0addcl  10089  un0mulcl  10090  nn0sub  10106  elz2  10132  zaddcl  10151  suprzcl2  10400  qmulz  10411  qre  10413  qnegcl  10425  xrmax1  10596  xrmin2  10599  max1ALT  10607  xlesubadd  10675  xmulass  10699  xlemul1a  10700  xrsupexmnf  10715  xrinfmexpnf  10716  xrub  10722  iccid  10793  fzsn  10925  fzsuc2  10934  fz1sbc  10951  elfzp12  10953  fzm1  10954  seqid3  11182  bcval5  11423  bcpasc  11426  hashbnd  11436  hashprg  11464  hashfzo  11479  cats1un  11572  shftlem  11659  replim  11697  absmod0  11884  absz  11892  rlimdm  12121  summolem2  12286  summo  12287  zsum  12288  fsum  12290  fsummulc2  12343  fsumconst  12349  fsum00  12353  incexclem  12392  isumsplit  12396  infcvgaux1i  12412  ruclem2  12607  fzo0dvdseq  12678  bitsf1ocnv  12732  sadcaddlem  12745  smueqlem  12778  gcdabs1  12810  bezoutlem1  12814  bezoutlem3  12816  bezoutlem4  12817  dvdsgcd  12819  dvdsmulgcd  12830  dvdsprime  12868  coprm  12876  isprm5  12888  prmdvdsexpr  12892  rpexp  12896  phibndlem  12935  dfphi2  12939  odzdvds  12957  pythagtriplem1  12966  iserodd  12985  pceulem  12995  pcqmul  13003  pcqcl  13006  pcxcl  13010  pcneg  13023  pcabs  13024  pcgcd1  13026  pcz  13030  pcprmpw2  13031  pcprmpw  13032  pcaddlem  13033  pcadd  13034  pcmpt  13037  pockthg  13050  prmreclem5  13064  4sqlem4  13096  mul4sq  13098  vdwapun  13118  vdwlem2  13126  vdwlem6  13130  vdwlem8  13132  vdwlem13  13137  0ram  13164  ram0  13166  ramcl  13173  wunress  13304  firest  13436  xpscfv  13563  isssc  13796  pospo  14206  latnlej  14273  gsumval2a  14558  mulgnn0p1  14677  mulgnn0ass  14695  gicsubgen  14841  mndodcongi  14957  oddvdsnn0  14958  odnncl  14959  oddvds  14961  odeq  14964  odeq1  14972  pgpfi2  15016  sylow2a  15029  sylow2blem3  15032  sylow3lem6  15042  lsmelvalm  15061  lsmsubm  15063  lsmsubg  15064  lsmmod  15083  lsmdisj2  15090  efgmnvl  15122  efgtlen  15134  efgs1b  15144  efgrelexlemb  15158  efgredeu  15160  efgcpbllemb  15163  frgpuptinv  15179  frgpup3lem  15185  divsabl  15256  frgpnabllem1  15260  cyggeninv  15269  cyggenod  15270  cygabl  15276  gsumval3eu  15289  dprdssv  15350  dprdfeq0  15356  dprdsubg  15358  dprddisj2  15373  ablfacrp  15400  pgpfac1lem3  15411  pgpfaclem2  15416  dvreq1  15574  irredn1  15587  drngmul0or  15632  isabvd  15684  abvdom  15702  issrngd  15725  lss1d  15819  lspsneq0  15868  lbspss  15934  lsmcl  15935  lvecvs0or  15960  lspindpi  15984  lidl1el  16069  lpiss  16101  lidldvgen  16106  nzrunit  16117  rrgeq0  16130  domneq0  16137  mplsubrglem  16282  mplmonmul  16307  coe1tmmul2  16451  coe1tmmul  16452  qsssubdrg  16537  zlpirlem1  16547  znfld  16620  znunit  16623  znrrg  16625  cygznlem3  16629  frgpcyg  16633  ipeq0  16648  cssincl  16694  lsmcss  16698  obselocv  16734  istopon  16769  eltg3  16806  tgidm  16824  clsval2  16893  opncldf1  16927  restbas  16995  tgrest  16996  restcld  17009  restcldr  17011  restcls  17017  restntr  17018  ordtbas2  17027  ordtbas  17028  ordtrest2lem  17039  ordtrest2  17040  pnfnei  17056  mnfnei  17057  tgcn  17088  cnconst  17118  cnindis  17126  lmss  17132  ordtt1  17213  discmp  17231  1stcrest  17285  2ndcdisj  17288  cldllycmp  17327  txbas  17368  ptpjpre1  17372  ptuni2  17377  ptbasin  17378  ptbasfi  17382  ptopn2  17385  txbasval  17407  ptpjopn  17412  ptclsg  17415  dfac14lem  17417  xkoccn  17419  ptcnp  17422  upxp  17423  ptrescn  17439  txkgen  17452  xkoptsub  17454  xkopt  17455  xkoco1cn  17457  xkoco2cn  17458  xkococn  17460  xkoinjcn  17487  ordthmeolem  17598  ptuncnv  17604  nrmhaus  17623  fbssint  17635  fbfinnfr  17638  fbasrn  17681  isufil2  17705  filufint  17717  rnelfm  17750  fmfnfmlem2  17752  fmfnfmlem3  17753  fmfnfmlem4  17754  fmfnfm  17755  flimtopon  17767  flimclslem  17781  fclstopon  17809  fclscf  17822  flimfnfcls  17825  alexsublem  17840  alexsubALTlem3  17845  alexsubALTlem4  17846  ptcmplem2  17849  tmdgsum2  17881  symgtgp  17886  cldsubg  17895  divstgplem  17905  tgptsmscld  17935  tsmsxplem1  17937  imasdsf1olem  18039  blss  18074  stdbdxmet  18163  methaus  18168  metrest  18172  nrginvrcn  18304  nmoeq0  18347  blssioo  18403  xrtgioo  18414  xrsxmet  18417  reconnlem1  18434  reconnlem2  18435  xrge0tsms  18442  elcncf1di  18502  iccpnfcnv  18546  evth  18561  lebnumlem1  18563  lebnumlem2  18564  lebnumlem3  18565  nmoleub3  18704  minveclem3b  18896  ivthlem2  18916  ivthlem3  18917  elovolm  18938  ovolmge0  18940  ovoliun  18968  ovolicc2lem3  18982  ovolicc2  18985  voliunlem3  19013  dyaddisj  19055  dyadmax  19057  opnmblALT  19062  ismbfd  19099  ismbf2d  19100  mbfimaopnlem  19114  mbfimaopn2  19116  i1fmullem  19153  i1fres  19164  itg1climres  19173  mbfi1fseqlem4  19177  itg2lcl  19186  itgsplitioo  19296  ellimc2  19331  rolle  19441  dvlip  19444  dvge0  19457  dvne0  19462  lhop1lem  19464  pf1ind  19542  tdeglem4  19550  degltlem1  19562  deg1nn0clb  19580  deg1lt0  19581  dvdsq1p  19650  ply1rem  19653  fta1g  19657  elply2  19682  plyf  19684  ne0p  19693  plyeq0lem  19696  plypf1  19698  0dgrb  19732  coe1termlem  19743  dgrcolem2  19759  plymul0or  19765  plyrem  19789  fta1  19792  quotcan  19793  aalioulem3  19818  eff1olem  20017  lognegb  20051  eflogeq  20063  argregt0  20072  argrege0  20073  tanarg  20081  cxpexp  20126  cxpeq0  20136  mulcxp  20143  cxpeq  20208  atans2  20338  scvxcvx  20391  isppw2  20465  vmappw  20466  vmacl  20468  efvmacl  20470  isnsqf  20485  mumullem2  20530  sqff1o  20532  dvdsppwf1o  20538  ppiublem1  20553  vmalelog  20556  chtublem  20562  fsumvma  20564  perfectlem2  20581  perfect  20582  bposlem1  20635  lgsmod  20672  lgsne0  20684  lgsdirnn0  20690  lgsqr  20697  lgsdchr  20699  lgseisenlem2  20701  lgsquadlem1  20705  lgsquadlem2  20706  2sqlem2  20715  mul2sq  20716  2sqlem7  20721  dchrisum0fno1  20772  pntrsumbnd2  20828  ostthlem1  20888  ostth2lem2  20895  ostth3  20899  ostth  20900  ismndo2  21124  ghgrplem1  21145  rngosn4  21206  nvmul0or  21324  ipasslem5  21527  ipasslem11  21532  hvmul0or  21718  his6  21792  hhssnv  21955  ocsh  21976  ocin  21989  shsidmi  22077  chnlen0  22137  h1de2bi  22247  h1de2ctlem  22248  h1de2ci  22249  spansni  22250  3oalem1  22355  nmcexi  22720  atcveq0  23042  chcv1  23049  cdjreui  23126  cdj3lem2b  23131  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  27479  nbgraf1olem1  27605  nbgraf1olem3  27607  nbgraf1olem5  27609  nb3graprlem2  27615  cusgrasize2inds  27640  vdgre1a  27813  vdusgra0nedg  27816  usgravd0nedg  27820  vdn0frgrav2  27857  vdgn0frgrav2  27858  bnj145  28517  nfsb4twAUX7  28997  nfsb4tOLD7  29146  nfsb4tw2AUXOLD7  29147  lshpdisj  29246  lsateln0  29254  lsatcveq0  29291  opnlen0  29447  glb0N  29452  cmtbr4N  29514  cvrnbtwn2  29534  cvrnbtwn4  29538  atcvreq0  29573  cvlatexch1  29595  exatleN  29662  atlelt  29696  ps-2  29736  llnn0  29774  lplnn0N  29805  islpln2a  29806  lvoln0N  29849  islvol2aN  29850  4at  29871  dalemcea  29918  dalem3  29922  pmapglb2N  30029  pmapglb2xN  30030  cdlema1N  30049  cdlemb  30052  paddasslem17  30094  llnexchb2lem  30126  llnexchb2  30127  lhpat3  30304  ltrnid  30393  trlne  30443  cdlemc4  30452  cdleme11h  30524  cdlemednuN  30558  cdlemg1a  30828  tendoeq2  31032  tendoid0  31083  dva1dim  31243  dib1dim  31424  dihlatat  31596  dochkrshp4  31648  dochkr1  31737  lclkrlem2e  31770  lcfrlem16  31817  lcfrlem28  31829  mapd0  31924  hdmap14lem13  32142
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