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  3183  eqsbc3r  3210  ordtr2  4617  ordsucss  4789  elreldm  5085  ssimaex  5779  fconstfv  5945  fliftfun  6025  isopolem  6056  isosolem  6058  f1oweALT  6065  fnse  6454  brtpos  6479  riotasvd  6583  issmo2  6602  seqomlem1  6698  omcl  6771  oecl  6772  oawordeulem  6788  oaass  6795  omordi  6800  omord  6802  odi  6813  oen0  6820  oeordi  6821  oeordsuc  6828  nnmcl  6846  nnecl  6847  nnmordi  6865  nnmord  6866  nnmwordri  6870  nnaordex  6872  swoord1  6925  ecopovtrn  6998  f1domg  7118  pw2f1olem  7203  domtriord  7244  mapen  7262  mapxpen  7264  mapunen  7267  nndomo  7291  inficl  7421  supmo  7446  inf3lem6  7577  cantnflem1  7634  tcmin  7669  tcrank  7797  cardne  7841  cardlim  7848  cardsdomel  7850  carduni  7857  alephord  7945  cardinfima  7967  dfac5lem4  7996  infdif2  8079  cofsmo  8138  cfcoflem  8141  infpssrlem4  8175  infpssrlem5  8176  fin4en1  8178  isfin2-2  8188  enfin2i  8190  fin23lem27  8197  isf32lem12  8233  isf34lem6  8249  domtriomlem  8311  cardmin  8428  fpwwe2lem12  8505  inar1  8639  gruiun  8663  ltsonq  8835  prub  8860  reclem3pr  8915  mulcmpblnr  8938  mulgt0sr  8969  axpre-sup  9033  leltadd  9501  infm3  9956  peano5nni  9992  zextle  10332  prime  10339  uzindOLD  10353  uzin  10507  ublbneg  10549  zbtwnre  10561  xrre2  10747  xralrple  10780  xmulneg1  10837  supxrbnd  10896  supxrgtmnf  10897  fzrevral  11119  flge  11202  ceile  11223  modadd1  11266  modmul1  11267  seqcl2  11329  facdiv  11566  hash2prb  11677  rlim2lt  12279  rlim3  12280  o1lo1  12319  climshftlem  12356  o1co  12368  o1of2  12394  isercolllem2  12447  isercoll  12449  caucvgrlem2  12456  climcndslem2  12618  sqr2irr  12836  dvds2lem  12850  dvdsle  12883  dvdsfac  12892  divalglem0  12901  ndvdsadd  12916  bitsinv1lem  12941  sadcaddlem  12957  dvdslegcd  13004  bezoutlem2  13027  bezoutlem4  13029  gcdeq  13040  algcvga  13058  prmind2  13078  isprm6  13097  rpexp  13108  rpdvds  13112  eulerthlem2  13159  pclem  13200  pceulem  13207  pc2dvds  13240  fldivp1  13254  infpnlem1  13266  prmunb  13270  mrieqv2d  13852  plttr  14415  joinlem  14435  meetlem  14442  issubg4  14949  gexdvds  15206  pgpssslw  15236  sylow2alem2  15240  efgs1b  15356  efgsfo  15359  lspindpi  16192  obselocv  16943  fiinbas  17005  bastg  17019  tgcl  17022  opnssneib  17167  clslp  17200  tgcnp  17305  iscnp4  17315  cncls2  17325  cncls  17326  cnntr  17327  cnpresti  17340  lmss  17350  lmcnp  17356  cmpsub  17451  tgcmp  17452  dfcon2  17470  t1conperf  17487  1stcfb  17496  1stcrest  17504  kgenss  17563  llycmpkgen2  17570  txdis  17652  qtoptop2  17719  kqt0lem  17756  isr0  17757  regr1lem2  17760  cmphaushmeo  17820  fbun  17860  ssfg  17892  fgtr  17910  ufildr  17951  cnpflf  18021  fclsnei  18039  flimfnfcls  18048  fclscmp  18050  ufilcmp  18052  cnpfcf  18061  alexsublem  18063  alexsubALTlem3  18068  alexsubALTlem4  18069  ptcmplem3  18073  tgphaus  18134  tgpt1  18135  tsmsres  18161  imasdsf1olem  18391  xblss2ps  18419  xblss2  18420  blsscls2  18522  metequiv2  18528  stdbdxmet  18533  nmoi  18750  reconn  18847  mulc1cncf  18923  cncfco  18925  iccpnfhmeo  18958  xrhmeo  18959  evth  18972  pi1grplem  19062  fgcfil  19212  ivthlem2  19337  ivthlem3  19338  ovolicc2lem4  19404  voliunlem1  19432  ioombl1lem4  19443  itg2gt0  19640  limcco  19768  lhop1  19886  pf1ind  19963  tdeglem4  19971  plypf1  20119  coeeulem  20131  coeidlem  20144  coeid3  20147  plymul0or  20186  dvnply2  20192  plydivex  20202  vieta1lem2  20216  plyexmo  20218  aaliou3lem2  20248  ulmss  20301  ulmdvlem3  20306  iblulm  20311  sincosq2sgn  20395  sincosq3sgn  20396  sincosq4sgn  20397  logcnlem5  20525  dcubic  20674  amgm  20817  isnsqf  20906  mumullem2  20951  chtublem  20983  chtub  20984  fsumvma2  20986  vmasum  20988  dchrfi  21027  bposlem1  21056  bposlem3  21058  bposlem7  21062  lgsdir  21102  lgsquadlem2  21127  2sqlem8a  21143  2sqlem10  21146  dchrisum0flb  21192  pntpbnd1  21268  pntlemf  21287  pntlem3  21291  umisuhgra  21350  uslisumgra  21374  usisuslgra  21375  constr3trl  21634  constr3pth  21635  vdusgraval  21666  gxcl  21841  isexid2  21901  lnon0  22287  normpyc  22636  ocsh  22773  ocorth  22781  ococss  22783  shsel2  22812  hsupss  22831  pjhth  22883  shlub  22904  cm2j  23110  lnfncnbd  23548  riesz1  23556  rnbra  23598  leopadd  23623  leopmuli  23624  hstles  23722  stge1i  23729  stle0i  23730  dmdbr5  23799  ssmd2  23803  superpos  23845  chcv1  23846  atoml2i  23874  chirredlem2  23882  atcvat3i  23887  mdsymlem5  23898  mdsymlem6  23899  sumdmdii  23906  sumdmdlem2  23910  sqsscirc2  24295  cnre2csqlem  24296  xrge0iifiso  24309  sigaclci  24503  ballotlemimin  24751  ballotlem7  24781  cvmlift2lem12  24989  dfon2lem8  25401  soseq  25509  axeuclid  25850  segconeq  25892  ifscgr  25926  brofs2  25959  brifs2  25960  endofsegid  25967  fzmul  26381  fdc  26386  incsequz2  26390  sstotbnd2  26420  sstotbnd3  26422  totbndbnd  26435  ispridl2  26585  irrapxlem2  26823  pell14qrdich  26869  monotoddzz  26943  pw2f1ocnv  27045  stoweidlem62  27725  elfzelfzccat  28079  swrdccatin12lem3  28099  swrdccatin12b  28102  swrdccat3b  28106  shwrdidxmod  28131  sbcim2g  28478  lsator0sp  29638  lssatle  29652  lshpset2N  29756  lkrlspeqN  29808  omllaw2N  29881  cmtbr3N  29891  lecmtN  29893  cvlcvr1  29976  cvrval4N  30050  cvrat3  30078  3noncolr2  30085  4noncolr3  30089  3dimlem3  30097  3dimlem3OLDN  30098  3dimlem4  30100  3dimlem4OLDN  30101  llncvrlpln  30194  lplncvrlvol  30252  snatpsubN  30386  linepsubN  30388  pmapjat1  30489  pclfinclN  30586  pl42N  30619  ltrneq2  30784  cdleme7aa  30878  cdleme18d  30931  cdleme21b  30962  trlord  31205  trlcoat  31359  dochkrshp  32023  lcfl8  32139
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