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  3205  eqsbc3r  3236  ordtr2  4750  elreldm  5051  ssimaex  5744  fconstfv  5927  fliftfun  5992  isopolem  6023  isosolem  6025  ordsucss  6418  f1oweALT  6550  fnse  6678  brtpos  6743  issmo2  6796  seqomlem1  6891  omcl  6964  oecl  6965  oawordeulem  6981  oaass  6988  omordi  6993  omord  6995  odi  7006  oen0  7013  oeordi  7014  oeordsuc  7021  nnmcl  7039  nnecl  7040  nnmordi  7058  nnmord  7059  nnmwordri  7063  nnaordex  7065  swoord1  7118  ecopovtrn  7191  f1domg  7317  pw2f1olem  7403  domtriord  7445  mapen  7463  mapxpen  7465  mapunen  7468  nndomo  7492  inficl  7663  supmo  7690  inf3lem6  7827  cantnflem1  7885  cantnflem1OLD  7908  tcmin  7949  tcrank  8079  cardne  8123  cardlim  8130  cardsdomel  8132  carduni  8139  alephord  8233  cardinfima  8255  dfac5lem4  8284  infdif2  8367  cofsmo  8426  cfcoflem  8429  infpssrlem4  8463  infpssrlem5  8464  fin4en1  8466  isfin2-2  8476  enfin2i  8478  fin23lem27  8485  isf32lem12  8521  isf34lem6  8537  domtriomlem  8599  cardmin  8716  fpwwe2lem12  8795  inar1  8929  gruiun  8953  ltsonq  9125  prub  9150  reclem3pr  9205  mulcmpblnr  9228  mulgt0sr  9259  axpre-sup  9323  leltadd  9810  infm3  10276  peano5nni  10312  zextle  10702  prime  10709  uzindOLD  10723  uzin  10880  ublbneg  10926  zbtwnre  10938  xrre2  11129  xralrple  11162  xmulneg1  11219  supxrbnd  11278  supxrgtmnf  11279  fzrevral  11527  flge  11638  ceile  11671  modadd1  11728  modmul1  11735  seqcl2  11807  facdiv  12046  hashss  12149  hash2prb  12163  elfzelfzccat  12262  repswswrd  12405  rlim2lt  12958  rlim3  12959  o1lo1  12998  climshftlem  13035  o1co  13047  o1of2  13073  isercolllem2  13126  isercoll  13128  caucvgrlem2  13135  climcndslem2  13295  sqr2irr  13513  dvds2lem  13527  dvdsle  13560  dvdsfac  13570  divalglem0  13579  ndvdsadd  13594  bitsinv1lem  13619  sadcaddlem  13635  dvdslegcd  13682  bezoutlem2  13705  bezoutlem4  13707  gcdeq  13718  algcvga  13736  prmind2  13756  isprm6  13777  rpexp  13788  rpdvds  13792  eulerthlem2  13839  pclem  13887  pceulem  13894  pc2dvds  13927  fldivp1  13941  infpnlem1  13953  prmunb  13957  mrieqv2d  14559  plttr  15122  clatl  15268  issubg4  15679  gexdvds  16062  pgpssslw  16092  sylow2alem2  16096  efgs1b  16212  efgsfo  16215  lspindpi  17134  psgnodpm  17859  psgndif  17873  obselocv  17994  mdetunilem9  18267  fiinbas  18398  bastg  18412  tgcl  18415  opnssneib  18560  clslp  18593  tgcnp  18698  iscnp4  18708  cncls2  18718  cncls  18719  cnntr  18720  cnpresti  18733  lmss  18743  lmcnp  18749  cmpsub  18844  tgcmp  18845  dfcon2  18864  t1conperf  18881  1stcfb  18890  1stcrest  18898  kgenss  18957  llycmpkgen2  18964  txdis  19046  qtoptop2  19113  kqt0lem  19150  isr0  19151  regr1lem2  19154  cmphaushmeo  19214  fbun  19254  ssfg  19286  fgtr  19304  ufildr  19345  cnpflf  19415  fclsnei  19433  flimfnfcls  19442  fclscmp  19444  ufilcmp  19446  cnpfcf  19455  alexsublem  19457  alexsubALTlem3  19462  alexsubALTlem4  19463  ptcmplem3  19467  tgphaus  19528  tgpt1  19529  tsmsresOLD  19558  tsmsres  19559  imasdsf1olem  19789  xblss2ps  19817  xblss2  19818  blsscls2  19920  metequiv2  19926  stdbdxmet  19931  nmoi  20148  reconn  20246  mulc1cncf  20322  cncfco  20324  iccpnfhmeo  20358  xrhmeo  20359  evth  20372  pi1grplem  20462  fgcfil  20623  ivthlem2  20777  ivthlem3  20778  ovolicc2lem4  20844  voliunlem1  20872  ioombl1lem4  20883  itg2gt0  21079  limcco  21209  lhop1  21327  pf1ind  21405  tdeglem4  21413  plypf1  21564  coeeulem  21576  coeidlem  21589  coeid3  21592  plymul0or  21631  dvnply2  21637  plydivex  21647  vieta1lem2  21661  plyexmo  21663  aaliou3lem2  21693  ulmss  21746  ulmdvlem3  21751  iblulm  21756  sincosq2sgn  21845  sincosq3sgn  21846  sincosq4sgn  21847  logcnlem5  21975  dcubic  22125  amgm  22268  isnsqf  22357  mumullem2  22402  chtublem  22434  chtub  22435  fsumvma2  22437  vmasum  22439  dchrfi  22478  bposlem1  22507  bposlem3  22509  bposlem7  22513  lgsdir  22553  lgsquadlem2  22578  2sqlem8a  22594  2sqlem10  22597  dchrisum0flb  22643  pntpbnd1  22719  pntlemf  22738  pntlem3  22742  axeuclid  23031  umisuhgra  23083  uslisumgra  23107  usisuslgra  23108  constr3trl  23367  constr3pth  23368  vdusgraval  23399  gxcl  23574  isexid2  23634  lnon0  24020  normpyc  24370  ocsh  24508  ocorth  24516  ococss  24518  shsel2  24547  hsupss  24566  pjhth  24618  shlub  24639  cm2j  24845  lnfncnbd  25283  riesz1  25291  rnbra  25333  leopadd  25358  leopmuli  25359  hstles  25457  stge1i  25464  stle0i  25465  dmdbr5  25534  ssmd2  25538  superpos  25580  chcv1  25581  atoml2i  25609  chirredlem2  25617  atcvat3i  25622  mdsymlem5  25633  mdsymlem6  25634  sumdmdii  25641  sumdmdlem2  25645  mul2lt0bi  25866  isarchiofld  26137  sqsscirc2  26192  cnre2csqlem  26193  xrge0iifiso  26218  sigaclci  26428  eulerpartlemb  26598  ballotlemimin  26735  ballotlem7  26765  cvmlift2lem12  27050  dfon2lem8  27449  soseq  27561  segconeq  27887  ifscgr  27921  brofs2  27954  brifs2  27955  endofsegid  27962  tan2h  28265  fzmul  28477  fdc  28482  incsequz2  28486  sstotbnd2  28514  sstotbnd3  28516  totbndbnd  28529  ispridl2  28679  irrapxlem2  29006  pell14qrdich  29052  monotoddzz  29126  pw2f1ocnv  29228  iocinico  29429  stoweidlem62  29700  elfzelfzlble  30052  wwlknext  30199  wwlkextsur  30206  clwwisshclwwlem1  30312  erclwwlktr0  30322  sbcim2g  30943  riotasvd  32177  lsator0sp  32216  lssatle  32230  lshpset2N  32334  lkrlspeqN  32386  omllaw2N  32459  cmtbr3N  32469  lecmtN  32471  cvlcvr1  32554  cvrval4N  32628  cvrat3  32656  3noncolr2  32663  4noncolr3  32667  3dimlem3  32675  3dimlem3OLDN  32676  3dimlem4  32678  3dimlem4OLDN  32679  llncvrlpln  32772  lplncvrlvol  32830  snatpsubN  32964  linepsubN  32966  pmapjat1  33067  pclfinclN  33164  pl42N  33197  ltrneq2  33362  cdleme7aa  33456  cdleme18d  33509  cdleme21b  33540  trlord  33783  trlcoat  33937  dochkrshp  34601  lcfl8  34717
  Copyright terms: Public domain W3C validator