MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylibrd Structured version   Visualization version   Unicode version

Theorem sylibrd 238
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylibrd.1  |-  ( ph  ->  ( ps  ->  ch ) )
sylibrd.2  |-  ( ph  ->  ( th  <->  ch )
)
Assertion
Ref Expression
sylibrd  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem sylibrd
StepHypRef Expression
1 sylibrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylibrd.2 . . 3  |-  ( ph  ->  ( th  <->  ch )
)
32biimprd 227 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 45 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  3imtr4d  272  sbciegft  3297  eqsbc3r  3323  elreldm  5058  ordtr2  5466  ssimaex  5928  fconstfvOLD  6125  fliftfun  6203  isopolem  6234  isosolem  6236  ordsucss  6642  f1oweALT  6774  fnse  6910  brtpos  6979  issmo2  7065  seqomlem1  7164  omcl  7235  oecl  7236  oawordeulem  7252  oaass  7259  omordi  7264  omord  7266  odi  7277  oen0  7284  oeordi  7285  oeordsuc  7292  nnmcl  7310  nnecl  7311  nnmordi  7329  nnmord  7330  nnmwordri  7334  nnaordex  7336  swoord1  7389  ecopovtrn  7463  f1domg  7586  pw2f1olem  7673  domtriord  7715  mapen  7733  mapxpen  7735  mapunen  7738  nndomo  7763  inficl  7936  supmo  7963  infmo  8008  inf3lem6  8135  cantnflem1  8191  tcmin  8222  tcrank  8352  cardne  8396  cardlim  8403  cardsdomel  8405  carduni  8412  alephord  8503  cardinfima  8525  dfac5lem4  8554  infdif2  8637  cofsmo  8696  cfcoflem  8699  infpssrlem4  8733  infpssrlem5  8734  fin4en1  8736  isfin2-2  8746  enfin2i  8748  fin23lem27  8755  isf32lem12  8791  isf34lem6  8807  domtriomlem  8869  cardmin  8986  fpwwe2lem12  9063  inar1  9197  gruiun  9221  ltsonq  9391  prub  9416  reclem3pr  9471  mulcmpblnr  9492  mulgt0sr  9526  axpre-sup  9590  leltadd  10095  infm3  10565  peano5nni  10609  zextle  11006  prime  11013  uzin  11188  ublbneg  11245  zbtwnre  11259  mul2lt0bi  11399  xrre2  11462  xralrple  11495  xmulneg1  11552  supxrbnd  11611  supxrgtmnf  11612  fzrevral  11876  flge  12038  ceile  12073  modadd1  12131  modmul1  12140  seqcl2  12228  facdiv  12469  hashss  12583  hash2exprb  12629  elfzelfzccat  12722  repswswrd  12882  cshwcsh2id  12922  rlim2lt  13554  rlim3  13555  o1lo1  13594  climshftlem  13631  o1co  13643  o1of2  13669  isercolllem2  13722  isercoll  13724  caucvgrlem2  13733  climcndslem2  13901  sqrt2irr  14294  dvds2lem  14308  dvdsle  14343  dvdsfac  14353  divalglem0  14364  ndvdsadd  14382  bitsinv1lem  14408  sadcaddlem  14424  dvdslegcd  14471  bezoutlem2OLD  14497  bezoutlem4OLD  14499  bezoutlem2  14500  bezoutlem4  14502  gcdeq  14513  algcvga  14531  prmind2  14628  isprm6  14659  rpexp  14665  rpdvds  14669  eulerthlem2  14723  pclem  14781  pceulem  14788  pc2dvds  14821  fldivp1  14835  infpnlem1  14847  prmunb  14851  mrieqv2d  15538  plttr  16209  clatl  16355  issubg4  16829  gexdvds  17228  pgpssslw  17259  sylow2alem2  17263  efgs1b  17379  efgsfo  17382  lspindpi  18348  pf1ind  18936  psgnodpm  19149  psgndif  19163  obselocv  19284  mdetunilem9  19638  fiinbas  19960  bastg  19974  tgcl  19978  opnssneib  20124  clslp  20157  tgcnp  20262  iscnp4  20272  cncls2  20282  cncls  20283  cnntr  20284  cnpresti  20297  lmss  20307  lmcnp  20313  cmpsub  20408  tgcmp  20409  dfcon2  20427  t1conperf  20444  1stcfb  20453  1stcrest  20461  kgenss  20551  llycmpkgen2  20558  txdis  20640  qtoptop2  20707  kqt0lem  20744  isr0  20745  regr1lem2  20748  cmphaushmeo  20808  fbun  20848  ssfg  20880  fgtr  20898  ufildr  20939  cnpflf  21009  fclsnei  21027  flimfnfcls  21036  fclscmp  21038  ufilcmp  21040  cnpfcf  21049  alexsublem  21052  alexsubALTlem3  21057  alexsubALTlem4  21058  ptcmplem3  21062  tgphaus  21124  tgpt1  21125  tsmsres  21151  imasdsf1olem  21381  xblss2ps  21409  xblss2  21410  blsscls2  21512  metequiv2  21518  stdbdxmet  21523  nmoi  21726  nmoiOLD  21742  reconn  21839  mulc1cncf  21930  cncfco  21932  iccpnfhmeo  21966  xrhmeo  21967  evth  21980  pi1grplem  22073  fgcfil  22234  ivthlem2  22396  ivthlem3  22397  ovolicc2lem4OLD  22466  ovolicc2lem4  22467  voliunlem1  22496  ioombl1lem4  22507  itg2gt0  22711  limcco  22841  lhop1  22959  tdeglem4  23002  plypf1  23159  coeeulem  23171  coeidlem  23184  coeid3  23187  plymul0or  23227  dvnply2  23233  plydivex  23243  vieta1lem2  23257  plyexmo  23259  aaliou3lem2  23292  ulmss  23345  ulmdvlem3  23350  iblulm  23355  sincosq2sgn  23447  sincosq3sgn  23448  sincosq4sgn  23449  logcnlem5  23584  dcubic  23765  amgm  23909  isnsqf  24055  mumullem2  24100  chtublem  24132  chtub  24133  fsumvma2  24135  vmasum  24137  dchrfi  24176  bposlem1  24205  bposlem3  24207  bposlem7  24211  lgsdir  24251  lgsquadlem2  24276  2sqlem8a  24292  2sqlem10  24295  dchrisum0flb  24341  pntpbnd1  24417  pntlemf  24436  pntlem3  24440  axeuclid  24986  umisuhgra  25047  uslisushgra  25083  uslisumgra  25084  usisuslgra  25085  constr3trl  25380  constr3pth  25381  wwlknext  25445  wwlkextsur  25452  clwwisshclwwlem1  25526  vdusgraval  25628  gxcl  25986  isexid2  26046  lnon0  26432  normpyc  26792  ocsh  26929  ocorth  26937  ococss  26939  shsel2  26968  hsupss  26987  pjhth  27039  shlub  27060  cm2j  27266  lnfncnbd  27703  riesz1  27711  rnbra  27753  leopadd  27778  leopmuli  27779  hstles  27877  stge1i  27884  stle0i  27885  dmdbr5  27954  ssmd2  27958  superpos  28000  chcv1  28001  atoml2i  28029  chirredlem2  28037  atcvat3i  28042  mdsymlem5  28053  mdsymlem6  28054  sumdmdii  28061  sumdmdlem2  28065  isarchiofld  28573  sqsscirc2  28708  cnre2csqlem  28709  xrge0iifiso  28734  sigaclci  28947  omssubadd  29121  omssubaddOLD  29125  eulerpartlemb  29194  ballotlemimin  29331  ballotlem7  29361  ballotlemiminOLD  29369  ballotlem7OLD  29399  cvmlift2lem12  30030  dfon2lem8  30429  soseq  30485  segconeq  30770  ifscgr  30804  brofs2  30837  brifs2  30838  endofsegid  30845  dissneqlem  31735  tan2h  31930  poimirlem31  31964  poimir  31966  fzmul  32062  fdc  32067  incsequz2  32071  sstotbnd2  32099  sstotbnd3  32101  totbndbnd  32114  ispridl2  32264  mpt2bi123f  32399  riotasvd  32522  lsator0sp  32561  lssatle  32575  lshpset2N  32679  lkrlspeqN  32731  omllaw2N  32804  cmtbr3N  32814  lecmtN  32816  cvlcvr1  32899  cvrval4N  32973  cvrat3  33001  3noncolr2  33008  4noncolr3  33012  3dimlem3  33020  3dimlem3OLDN  33021  3dimlem4  33023  3dimlem4OLDN  33024  llncvrlpln  33117  lplncvrlvol  33175  snatpsubN  33309  linepsubN  33311  pmapjat1  33412  pclfinclN  33509  pl42N  33542  ltrneq2  33707  cdleme7aa  33802  cdleme18d  33855  cdleme21b  33887  trlord  34130  trlcoat  34284  dochkrshp  34948  lcfl8  35064  irrapxlem2  35661  pell14qrdich  35709  monotoddzz  35785  pw2f1ocnv  35886  iocinico  36090  sbcim2g  36893  stoweidlem62  37917  stoweidlem62OLD  37918  gcdzeq  38787  elfzelfzlble  39048  uspgrushgr  39248  uspgrupgr  39249  usgruspgr  39251
  Copyright terms: Public domain W3C validator