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

Theorem sylibrd 226
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 215 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 42 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr4d  260  sbciegft  3151  eqsbc3r  3178  ordtr2  4585  ordsucss  4757  elreldm  5053  ssimaex  5747  fconstfv  5913  fliftfun  5993  isopolem  6024  isosolem  6026  f1oweALT  6033  fnse  6422  brtpos  6447  riotasvd  6551  issmo2  6570  seqomlem1  6666  omcl  6739  oecl  6740  oawordeulem  6756  oaass  6763  omordi  6768  omord  6770  odi  6781  oen0  6788  oeordi  6789  oeordsuc  6796  nnmcl  6814  nnecl  6815  nnmordi  6833  nnmord  6834  nnmwordri  6838  nnaordex  6840  swoord1  6893  ecopovtrn  6966  f1domg  7086  pw2f1olem  7171  domtriord  7212  mapen  7230  mapxpen  7232  mapunen  7235  nndomo  7259  inficl  7388  supmo  7413  inf3lem6  7544  cantnflem1  7601  tcmin  7636  tcrank  7764  cardne  7808  cardlim  7815  cardsdomel  7817  carduni  7824  alephord  7912  cardinfima  7934  dfac5lem4  7963  infdif2  8046  cofsmo  8105  cfcoflem  8108  infpssrlem4  8142  infpssrlem5  8143  fin4en1  8145  isfin2-2  8155  enfin2i  8157  fin23lem27  8164  isf32lem12  8200  isf34lem6  8216  domtriomlem  8278  cardmin  8395  fpwwe2lem12  8472  inar1  8606  gruiun  8630  ltsonq  8802  prub  8827  reclem3pr  8882  mulcmpblnr  8905  mulgt0sr  8936  axpre-sup  9000  leltadd  9468  infm3  9923  peano5nni  9959  zextle  10299  prime  10306  uzindOLD  10320  uzin  10474  ublbneg  10516  zbtwnre  10528  xrre2  10714  xralrple  10747  xmulneg1  10804  supxrbnd  10863  supxrgtmnf  10864  fzrevral  11086  flge  11169  ceile  11190  modadd1  11233  modmul1  11234  seqcl2  11296  facdiv  11533  hash2prb  11644  rlim2lt  12246  rlim3  12247  o1lo1  12286  climshftlem  12323  o1co  12335  o1of2  12361  isercolllem2  12414  isercoll  12416  caucvgrlem2  12423  climcndslem2  12585  sqr2irr  12803  dvds2lem  12817  dvdsle  12850  dvdsfac  12859  divalglem0  12868  ndvdsadd  12883  bitsinv1lem  12908  sadcaddlem  12924  dvdslegcd  12971  bezoutlem2  12994  bezoutlem4  12996  gcdeq  13007  algcvga  13025  prmind2  13045  isprm6  13064  rpexp  13075  rpdvds  13079  eulerthlem2  13126  pclem  13167  pceulem  13174  pc2dvds  13207  fldivp1  13221  infpnlem1  13233  prmunb  13237  mrieqv2d  13819  plttr  14382  joinlem  14402  meetlem  14409  issubg4  14916  gexdvds  15173  pgpssslw  15203  sylow2alem2  15207  efgs1b  15323  efgsfo  15326  lspindpi  16159  obselocv  16910  fiinbas  16972  bastg  16986  tgcl  16989  opnssneib  17134  clslp  17166  tgcnp  17271  iscnp4  17281  cncls2  17291  cncls  17292  cnntr  17293  cnpresti  17306  lmss  17316  lmcnp  17322  cmpsub  17417  tgcmp  17418  dfcon2  17435  t1conperf  17452  1stcfb  17461  1stcrest  17469  kgenss  17528  llycmpkgen2  17535  txdis  17617  qtoptop2  17684  kqt0lem  17721  isr0  17722  regr1lem2  17725  cmphaushmeo  17785  fbun  17825  ssfg  17857  fgtr  17875  ufildr  17916  cnpflf  17986  fclsnei  18004  flimfnfcls  18013  fclscmp  18015  ufilcmp  18017  cnpfcf  18026  alexsublem  18028  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem3  18038  tgphaus  18099  tgpt1  18100  tsmsres  18126  imasdsf1olem  18356  xblss2ps  18384  xblss2  18385  blsscls2  18487  metequiv2  18493  stdbdxmet  18498  nmoi  18715  reconn  18812  mulc1cncf  18888  cncfco  18890  iccpnfhmeo  18923  xrhmeo  18924  evth  18937  pi1grplem  19027  fgcfil  19177  ivthlem2  19302  ivthlem3  19303  ovolicc2lem4  19369  voliunlem1  19397  ioombl1lem4  19408  itg2gt0  19605  limcco  19733  lhop1  19851  pf1ind  19928  tdeglem4  19936  plypf1  20084  coeeulem  20096  coeidlem  20109  coeid3  20112  plymul0or  20151  dvnply2  20157  plydivex  20167  vieta1lem2  20181  plyexmo  20183  aaliou3lem2  20213  ulmss  20266  ulmdvlem3  20271  iblulm  20276  sincosq2sgn  20360  sincosq3sgn  20361  sincosq4sgn  20362  logcnlem5  20490  dcubic  20639  amgm  20782  isnsqf  20871  mumullem2  20916  chtublem  20948  chtub  20949  fsumvma2  20951  vmasum  20953  dchrfi  20992  bposlem1  21021  bposlem3  21023  bposlem7  21027  lgsdir  21067  lgsquadlem2  21092  2sqlem8a  21108  2sqlem10  21111  dchrisum0flb  21157  pntpbnd1  21233  pntlemf  21252  pntlem3  21256  umisuhgra  21315  uslisumgra  21339  usisuslgra  21340  constr3trl  21599  constr3pth  21600  vdusgraval  21631  gxcl  21806  isexid2  21866  lnon0  22252  normpyc  22601  ocsh  22738  ocorth  22746  ococss  22748  shsel2  22777  hsupss  22796  pjhth  22848  shlub  22869  cm2j  23075  lnfncnbd  23513  riesz1  23521  rnbra  23563  leopadd  23588  leopmuli  23589  hstles  23687  stge1i  23694  stle0i  23695  dmdbr5  23764  ssmd2  23768  superpos  23810  chcv1  23811  atoml2i  23839  chirredlem2  23847  atcvat3i  23852  mdsymlem5  23863  mdsymlem6  23864  sumdmdii  23871  sumdmdlem2  23875  sqsscirc2  24260  cnre2csqlem  24261  xrge0iifiso  24274  sigaclci  24468  ballotlemimin  24716  ballotlem7  24746  cvmlift2lem12  24954  dfon2lem8  25360  soseq  25468  axeuclid  25806  segconeq  25848  ifscgr  25882  brofs2  25915  brifs2  25916  endofsegid  25923  fzmul  26334  fdc  26339  incsequz2  26343  sstotbnd2  26373  sstotbnd3  26375  totbndbnd  26388  ispridl2  26538  irrapxlem2  26776  pell14qrdich  26822  monotoddzz  26896  pw2f1ocnv  26998  stoweidlem62  27678  elfzelfzccat  28006  swrdccatin12lem3  28024  swrdccatin12b  28027  swrdccat3b  28031  sbcim2g  28334  lsator0sp  29484  lssatle  29498  lshpset2N  29602  lkrlspeqN  29654  omllaw2N  29727  cmtbr3N  29737  lecmtN  29739  cvlcvr1  29822  cvrval4N  29896  cvrat3  29924  3noncolr2  29931  4noncolr3  29935  3dimlem3  29943  3dimlem3OLDN  29944  3dimlem4  29946  3dimlem4OLDN  29947  llncvrlpln  30040  lplncvrlvol  30098  snatpsubN  30232  linepsubN  30234  pmapjat1  30335  pclfinclN  30432  pl42N  30465  ltrneq2  30630  cdleme7aa  30724  cdleme18d  30777  cdleme21b  30808  trlord  31051  trlcoat  31205  dochkrshp  31869  lcfl8  31985
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 178
  Copyright terms: Public domain W3C validator