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 44 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  3344  eqsbc3r  3375  ordtr2  4912  elreldm  5217  ssimaex  5923  fconstfvOLD  6119  fliftfun  6195  isopolem  6226  isosolem  6228  ordsucss  6638  f1oweALT  6769  fnse  6902  brtpos  6966  issmo2  7022  seqomlem1  7117  omcl  7188  oecl  7189  oawordeulem  7205  oaass  7212  omordi  7217  omord  7219  odi  7230  oen0  7237  oeordi  7238  oeordsuc  7245  nnmcl  7263  nnecl  7264  nnmordi  7282  nnmord  7283  nnmwordri  7287  nnaordex  7289  swoord1  7342  ecopovtrn  7416  f1domg  7537  pw2f1olem  7623  domtriord  7665  mapen  7683  mapxpen  7685  mapunen  7688  nndomo  7713  inficl  7887  supmo  7914  inf3lem6  8053  cantnflem1  8111  cantnflem1OLD  8134  tcmin  8175  tcrank  8305  cardne  8349  cardlim  8356  cardsdomel  8358  carduni  8365  alephord  8459  cardinfima  8481  dfac5lem4  8510  infdif2  8593  cofsmo  8652  cfcoflem  8655  infpssrlem4  8689  infpssrlem5  8690  fin4en1  8692  isfin2-2  8702  enfin2i  8704  fin23lem27  8711  isf32lem12  8747  isf34lem6  8763  domtriomlem  8825  cardmin  8942  fpwwe2lem12  9022  inar1  9156  gruiun  9180  ltsonq  9350  prub  9375  reclem3pr  9430  mulcmpblnr  9451  mulgt0sr  9485  axpre-sup  9549  leltadd  10043  infm3  10509  peano5nni  10546  zextle  10943  prime  10950  uzindOLD  10964  uzin  11123  ublbneg  11176  zbtwnre  11190  xrre2  11381  xralrple  11414  xmulneg1  11471  supxrbnd  11530  supxrgtmnf  11531  fzrevral  11773  flge  11923  ceile  11957  modadd1  12014  modmul1  12021  seqcl2  12106  facdiv  12346  hashss  12455  hash2prb  12498  elfzelfzccat  12579  repswswrd  12737  cshwcsh2id  12777  rlim2lt  13301  rlim3  13302  o1lo1  13341  climshftlem  13378  o1co  13390  o1of2  13416  isercolllem2  13469  isercoll  13471  caucvgrlem2  13478  climcndslem2  13643  sqrt2irr  13963  dvds2lem  13977  dvdsle  14012  dvdsfac  14022  divalglem0  14032  ndvdsadd  14047  bitsinv1lem  14072  sadcaddlem  14088  dvdslegcd  14135  bezoutlem2  14158  bezoutlem4  14160  gcdeq  14171  algcvga  14189  prmind2  14209  isprm6  14231  rpexp  14242  rpdvds  14246  eulerthlem2  14293  pclem  14343  pceulem  14350  pc2dvds  14383  fldivp1  14397  infpnlem1  14409  prmunb  14413  mrieqv2d  15017  plttr  15578  clatl  15724  issubg4  16198  gexdvds  16582  pgpssslw  16612  sylow2alem2  16616  efgs1b  16732  efgsfo  16735  lspindpi  17756  pf1ind  18369  psgnodpm  18601  psgndif  18615  obselocv  18736  mdetunilem9  19099  fiinbas  19430  bastg  19444  tgcl  19448  opnssneib  19593  clslp  19626  tgcnp  19731  iscnp4  19741  cncls2  19751  cncls  19752  cnntr  19753  cnpresti  19766  lmss  19776  lmcnp  19782  cmpsub  19877  tgcmp  19878  dfcon2  19897  t1conperf  19914  1stcfb  19923  1stcrest  19931  kgenss  20021  llycmpkgen2  20028  txdis  20110  qtoptop2  20177  kqt0lem  20214  isr0  20215  regr1lem2  20218  cmphaushmeo  20278  fbun  20318  ssfg  20350  fgtr  20368  ufildr  20409  cnpflf  20479  fclsnei  20497  flimfnfcls  20506  fclscmp  20508  ufilcmp  20510  cnpfcf  20519  alexsublem  20521  alexsubALTlem3  20526  alexsubALTlem4  20527  ptcmplem3  20531  tgphaus  20592  tgpt1  20593  tsmsresOLD  20622  tsmsres  20623  imasdsf1olem  20853  xblss2ps  20881  xblss2  20882  blsscls2  20984  metequiv2  20990  stdbdxmet  20995  nmoi  21212  reconn  21310  mulc1cncf  21386  cncfco  21388  iccpnfhmeo  21422  xrhmeo  21423  evth  21436  pi1grplem  21526  fgcfil  21687  ivthlem2  21841  ivthlem3  21842  ovolicc2lem4  21908  voliunlem1  21937  ioombl1lem4  21948  itg2gt0  22144  limcco  22274  lhop1  22392  tdeglem4  22435  plypf1  22586  coeeulem  22598  coeidlem  22611  coeid3  22614  plymul0or  22653  dvnply2  22659  plydivex  22669  vieta1lem2  22683  plyexmo  22685  aaliou3lem2  22715  ulmss  22768  ulmdvlem3  22773  iblulm  22778  sincosq2sgn  22868  sincosq3sgn  22869  sincosq4sgn  22870  logcnlem5  23003  dcubic  23153  amgm  23296  isnsqf  23385  mumullem2  23430  chtublem  23462  chtub  23463  fsumvma2  23465  vmasum  23467  dchrfi  23506  bposlem1  23535  bposlem3  23537  bposlem7  23541  lgsdir  23581  lgsquadlem2  23606  2sqlem8a  23622  2sqlem10  23625  dchrisum0flb  23671  pntpbnd1  23747  pntlemf  23766  pntlem3  23770  axeuclid  24242  umisuhgra  24303  uslisushgra  24339  uslisumgra  24340  usisuslgra  24341  constr3trl  24635  constr3pth  24636  wwlknext  24700  wwlkextsur  24707  clwwisshclwwlem1  24781  vdusgraval  24883  gxcl  25243  isexid2  25303  lnon0  25689  normpyc  26039  ocsh  26177  ocorth  26185  ococss  26187  shsel2  26216  hsupss  26235  pjhth  26287  shlub  26308  cm2j  26514  lnfncnbd  26952  riesz1  26960  rnbra  27002  leopadd  27027  leopmuli  27028  hstles  27126  stge1i  27133  stle0i  27134  dmdbr5  27203  ssmd2  27207  superpos  27249  chcv1  27250  atoml2i  27278  chirredlem2  27286  atcvat3i  27291  mdsymlem5  27302  mdsymlem6  27303  sumdmdii  27310  sumdmdlem2  27314  mul2lt0bi  27545  isarchiofld  27784  sqsscirc2  27868  cnre2csqlem  27869  xrge0iifiso  27894  sigaclci  28109  eulerpartlemb  28284  ballotlemimin  28421  ballotlem7  28451  cvmlift2lem12  28736  dfon2lem8  29197  soseq  29309  segconeq  29635  ifscgr  29669  brofs2  29702  brifs2  29703  endofsegid  29710  tan2h  30022  fzmul  30208  fdc  30213  incsequz2  30217  sstotbnd2  30245  sstotbnd3  30247  totbndbnd  30260  ispridl2  30410  mpt2bi123f  30546  irrapxlem2  30734  pell14qrdich  30780  monotoddzz  30854  pw2f1ocnv  30954  iocinico  31155  stoweidlem62  31733  elfzelfzlble  32175  sbcim2g  33042  riotasvd  34427  lsator0sp  34466  lssatle  34480  lshpset2N  34584  lkrlspeqN  34636  omllaw2N  34709  cmtbr3N  34719  lecmtN  34721  cvlcvr1  34804  cvrval4N  34878  cvrat3  34906  3noncolr2  34913  4noncolr3  34917  3dimlem3  34925  3dimlem3OLDN  34926  3dimlem4  34928  3dimlem4OLDN  34929  llncvrlpln  35022  lplncvrlvol  35080  snatpsubN  35214  linepsubN  35216  pmapjat1  35317  pclfinclN  35414  pl42N  35447  ltrneq2  35612  cdleme7aa  35707  cdleme18d  35760  cdleme21b  35792  trlord  36035  trlcoat  36189  dochkrshp  36853  lcfl8  36969
  Copyright terms: Public domain W3C validator