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

Theorem sylibrd 234
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 223 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 42 1  |-  ( ph  ->  ( ps  ->  th )
)
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:  3imtr4d  268  sbciegft  3307  eqsbc3r  3333  elreldm  5047  ordtr2  5453  ssimaex  5913  fconstfvOLD  6114  fliftfun  6192  isopolem  6223  isosolem  6225  ordsucss  6635  f1oweALT  6767  fnse  6900  brtpos  6966  issmo2  7052  seqomlem1  7151  omcl  7222  oecl  7223  oawordeulem  7239  oaass  7246  omordi  7251  omord  7253  odi  7264  oen0  7271  oeordi  7272  oeordsuc  7279  nnmcl  7297  nnecl  7298  nnmordi  7316  nnmord  7317  nnmwordri  7321  nnaordex  7323  swoord1  7376  ecopovtrn  7450  f1domg  7572  pw2f1olem  7658  domtriord  7700  mapen  7718  mapxpen  7720  mapunen  7723  nndomo  7748  inficl  7918  supmo  7944  inf3lem6  8082  cantnflem1  8139  cantnflem1OLD  8162  tcmin  8203  tcrank  8333  cardne  8377  cardlim  8384  cardsdomel  8386  carduni  8393  alephord  8487  cardinfima  8509  dfac5lem4  8538  infdif2  8621  cofsmo  8680  cfcoflem  8683  infpssrlem4  8717  infpssrlem5  8718  fin4en1  8720  isfin2-2  8730  enfin2i  8732  fin23lem27  8739  isf32lem12  8775  isf34lem6  8791  domtriomlem  8853  cardmin  8970  fpwwe2lem12  9048  inar1  9182  gruiun  9206  ltsonq  9376  prub  9401  reclem3pr  9456  mulcmpblnr  9477  mulgt0sr  9511  axpre-sup  9575  leltadd  10076  infm3  10541  peano5nni  10578  zextle  10976  prime  10983  uzin  11158  ublbneg  11210  zbtwnre  11224  mul2lt0bi  11363  xrre2  11423  xralrple  11456  xmulneg1  11513  supxrbnd  11572  supxrgtmnf  11573  fzrevral  11816  flge  11977  ceile  12012  modadd1  12070  modmul1  12079  seqcl2  12167  facdiv  12407  hashss  12521  hash2prb  12564  elfzelfzccat  12650  repswswrd  12810  cshwcsh2id  12850  rlim2lt  13467  rlim3  13468  o1lo1  13507  climshftlem  13544  o1co  13556  o1of2  13582  isercolllem2  13635  isercoll  13637  caucvgrlem2  13644  climcndslem2  13811  sqrt2irr  14189  dvds2lem  14203  dvdsle  14238  dvdsfac  14248  divalglem0  14258  ndvdsadd  14273  bitsinv1lem  14298  sadcaddlem  14314  dvdslegcd  14361  bezoutlem2  14384  bezoutlem4  14386  gcdeq  14397  algcvga  14415  prmind2  14435  isprm6  14457  rpexp  14468  rpdvds  14472  eulerthlem2  14519  pclem  14569  pceulem  14576  pc2dvds  14609  fldivp1  14623  infpnlem1  14635  prmunb  14639  mrieqv2d  15251  plttr  15922  clatl  16068  issubg4  16542  gexdvds  16926  pgpssslw  16956  sylow2alem2  16960  efgs1b  17076  efgsfo  17079  lspindpi  18096  pf1ind  18709  psgnodpm  18920  psgndif  18934  obselocv  19055  mdetunilem9  19412  fiinbas  19743  bastg  19757  tgcl  19761  opnssneib  19907  clslp  19940  tgcnp  20045  iscnp4  20055  cncls2  20065  cncls  20066  cnntr  20067  cnpresti  20080  lmss  20090  lmcnp  20096  cmpsub  20191  tgcmp  20192  dfcon2  20210  t1conperf  20227  1stcfb  20236  1stcrest  20244  kgenss  20334  llycmpkgen2  20341  txdis  20423  qtoptop2  20490  kqt0lem  20527  isr0  20528  regr1lem2  20531  cmphaushmeo  20591  fbun  20631  ssfg  20663  fgtr  20681  ufildr  20722  cnpflf  20792  fclsnei  20810  flimfnfcls  20819  fclscmp  20821  ufilcmp  20823  cnpfcf  20832  alexsublem  20834  alexsubALTlem3  20839  alexsubALTlem4  20840  ptcmplem3  20844  tgphaus  20905  tgpt1  20906  tsmsresOLD  20935  tsmsres  20936  imasdsf1olem  21166  xblss2ps  21194  xblss2  21195  blsscls2  21297  metequiv2  21303  stdbdxmet  21308  nmoi  21525  reconn  21623  mulc1cncf  21699  cncfco  21701  iccpnfhmeo  21735  xrhmeo  21736  evth  21749  pi1grplem  21839  fgcfil  22000  ivthlem2  22154  ivthlem3  22155  ovolicc2lem4  22221  voliunlem1  22250  ioombl1lem4  22261  itg2gt0  22457  limcco  22587  lhop1  22705  tdeglem4  22748  plypf1  22899  coeeulem  22911  coeidlem  22924  coeid3  22927  plymul0or  22967  dvnply2  22973  plydivex  22983  vieta1lem2  22997  plyexmo  22999  aaliou3lem2  23029  ulmss  23082  ulmdvlem3  23087  iblulm  23092  sincosq2sgn  23182  sincosq3sgn  23183  sincosq4sgn  23184  logcnlem5  23319  dcubic  23500  amgm  23644  isnsqf  23788  mumullem2  23833  chtublem  23865  chtub  23866  fsumvma2  23868  vmasum  23870  dchrfi  23909  bposlem1  23938  bposlem3  23940  bposlem7  23944  lgsdir  23984  lgsquadlem2  24009  2sqlem8a  24025  2sqlem10  24028  dchrisum0flb  24074  pntpbnd1  24150  pntlemf  24169  pntlem3  24173  axeuclid  24670  umisuhgra  24731  uslisushgra  24767  uslisumgra  24768  usisuslgra  24769  constr3trl  25063  constr3pth  25064  wwlknext  25128  wwlkextsur  25135  clwwisshclwwlem1  25209  vdusgraval  25311  gxcl  25667  isexid2  25727  lnon0  26113  normpyc  26463  ocsh  26601  ocorth  26609  ococss  26611  shsel2  26640  hsupss  26659  pjhth  26711  shlub  26732  cm2j  26938  lnfncnbd  27375  riesz1  27383  rnbra  27425  leopadd  27450  leopmuli  27451  hstles  27549  stge1i  27556  stle0i  27557  dmdbr5  27626  ssmd2  27630  superpos  27672  chcv1  27673  atoml2i  27701  chirredlem2  27709  atcvat3i  27714  mdsymlem5  27725  mdsymlem6  27726  sumdmdii  27733  sumdmdlem2  27737  isarchiofld  28246  sqsscirc2  28330  cnre2csqlem  28331  xrge0iifiso  28356  sigaclci  28566  omssubadd  28734  eulerpartlemb  28799  ballotlemimin  28936  ballotlem7  28966  cvmlift2lem12  29598  dfon2lem8  29996  soseq  30052  segconeq  30335  ifscgr  30369  brofs2  30402  brifs2  30403  endofsegid  30410  dissneqlem  31243  tan2h  31399  fzmul  31495  fdc  31500  incsequz2  31504  sstotbnd2  31532  sstotbnd3  31534  totbndbnd  31547  ispridl2  31697  mpt2bi123f  31833  riotasvd  31960  lsator0sp  31999  lssatle  32013  lshpset2N  32117  lkrlspeqN  32169  omllaw2N  32242  cmtbr3N  32252  lecmtN  32254  cvlcvr1  32337  cvrval4N  32411  cvrat3  32439  3noncolr2  32446  4noncolr3  32450  3dimlem3  32458  3dimlem3OLDN  32459  3dimlem4  32461  3dimlem4OLDN  32462  llncvrlpln  32555  lplncvrlvol  32613  snatpsubN  32747  linepsubN  32749  pmapjat1  32850  pclfinclN  32947  pl42N  32980  ltrneq2  33145  cdleme7aa  33240  cdleme18d  33293  cdleme21b  33325  trlord  33568  trlcoat  33722  dochkrshp  34386  lcfl8  34502  irrapxlem2  35100  pell14qrdich  35146  monotoddzz  35220  pw2f1ocnv  35321  iocinico  35523  sbcim2g  36309  stoweidlem62  37193  gcdzeq  37727  elfzelfzlble  37950
  Copyright terms: Public domain W3C validator