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

Theorem sylibrd 225
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 214 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 40 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr4d  259  sbciegft  3097  eqsbc3r  3124  ordtr2  4518  ordsucss  4691  elreldm  4985  ssimaex  5667  fconstfv  5820  fliftfun  5898  isopolem  5929  isosolem  5931  f1oweALT  5938  fnse  6319  brtpos  6330  riotasvd  6434  issmo2  6453  seqomlem1  6549  omcl  6622  oecl  6623  oawordeulem  6639  oaass  6646  omordi  6651  omord  6653  odi  6664  oen0  6671  oeordi  6672  oeordsuc  6679  nnmcl  6697  nnecl  6698  nnmordi  6716  nnmord  6717  nnmwordri  6721  nnaordex  6723  swoord1  6776  ecopovtrn  6849  f1domg  6969  pw2f1olem  7054  domtriord  7095  mapen  7113  mapxpen  7115  mapunen  7118  nndomo  7142  inficl  7268  supmo  7293  inf3lem6  7424  cantnflem1  7481  tcmin  7516  tcrank  7644  cardne  7688  cardlim  7695  cardsdomel  7697  carduni  7704  alephord  7792  cardinfima  7814  dfac5lem4  7843  infdif2  7926  cofsmo  7985  cfcoflem  7988  infpssrlem4  8022  infpssrlem5  8023  fin4en1  8025  isfin2-2  8035  enfin2i  8037  fin23lem27  8044  isf32lem12  8080  isf34lem6  8096  domtriomlem  8158  cardmin  8276  fpwwe2lem12  8353  inar1  8487  gruiun  8511  ltsonq  8683  prub  8708  reclem3pr  8763  mulcmpblnr  8786  mulgt0sr  8817  axpre-sup  8881  leltadd  9348  infm3  9803  peano5nni  9839  zextle  10177  prime  10184  uzindOLD  10198  uzin  10352  ublbneg  10394  zbtwnre  10406  xrre2  10591  xralrple  10624  xmulneg1  10681  supxrbnd  10739  supxrgtmnf  10740  fzrevral  10958  flge  11029  ceile  11050  modadd1  11093  modmul1  11094  seqcl2  11156  facdiv  11393  rlim2lt  12067  rlim3  12068  o1lo1  12107  climshftlem  12144  o1co  12156  o1of2  12182  isercolllem2  12235  isercoll  12237  caucvgrlem2  12244  climcndslem2  12406  sqr2irr  12624  dvds2lem  12638  dvdsle  12671  dvdsfac  12680  divalglem0  12689  ndvdsadd  12704  bitsinv1lem  12729  sadcaddlem  12745  dvdslegcd  12792  bezoutlem2  12815  bezoutlem4  12817  gcdeq  12828  algcvga  12846  prmind2  12866  isprm6  12885  rpexp  12896  rpdvds  12900  eulerthlem2  12947  pclem  12988  pceulem  12995  pc2dvds  13028  fldivp1  13042  infpnlem1  13054  prmunb  13058  mrieqv2d  13640  plttr  14203  joinlem  14223  meetlem  14230  issubg4  14737  gexdvds  14994  pgpssslw  15024  sylow2alem2  15028  efgs1b  15144  efgsfo  15147  lspindpi  15984  obselocv  16734  fiinbas  16796  bastg  16810  tgcl  16813  opnssneib  16958  clslp  16985  tgcnp  17089  cncls2  17108  cncls  17109  cnntr  17110  cnpresti  17122  lmss  17132  lmcnp  17138  cmpsub  17233  tgcmp  17234  dfcon2  17251  t1conperf  17268  1stcfb  17277  1stcrest  17285  kgenss  17344  llycmpkgen2  17351  txdis  17432  qtoptop2  17496  kqt0lem  17533  isr0  17534  regr1lem2  17537  cmphaushmeo  17597  fbun  17637  ssfg  17669  fgtr  17687  ufildr  17728  cnpflf  17798  fclsnei  17816  flimfnfcls  17825  fclscmp  17827  ufilcmp  17829  cnpfcf  17838  alexsublem  17840  alexsubALTlem3  17845  alexsubALTlem4  17846  ptcmplem3  17850  tgphaus  17901  tgpt1  17902  tsmsres  17928  imasdsf1olem  18039  xblss2  18060  blsscls2  18152  metequiv2  18158  stdbdxmet  18163  nmoi  18339  reconn  18436  mulc1cncf  18512  cncfco  18514  iccpnfhmeo  18547  xrhmeo  18548  evth  18561  pi1grplem  18651  fgcfil  18801  ivthlem2  18916  ivthlem3  18917  ovolicc2lem4  18983  voliunlem1  19011  ioombl1lem4  19022  itg2gt0  19219  limcco  19347  lhop1  19465  pf1ind  19542  tdeglem4  19550  plypf1  19698  coeeulem  19710  coeidlem  19723  coeid3  19726  plymul0or  19765  dvnply2  19771  plydivex  19781  vieta1lem2  19795  plyexmo  19797  aaliou3lem2  19827  ulmss  19880  ulmdvlem3  19885  iblulm  19890  sincosq2sgn  19974  sincosq3sgn  19975  sincosq4sgn  19976  logcnlem5  20104  dcubic  20253  amgm  20396  isnsqf  20485  mumullem2  20530  chtublem  20562  chtub  20563  fsumvma2  20565  vmasum  20567  dchrfi  20606  bposlem1  20635  bposlem3  20637  bposlem7  20641  lgsdir  20681  lgsquadlem2  20706  2sqlem8a  20722  2sqlem10  20725  dchrisum0flb  20771  pntpbnd1  20847  pntlemf  20866  pntlem3  20870  gxcl  21044  isexid2  21104  lnon0  21490  normpyc  21839  ocsh  21976  ocorth  21984  ococss  21986  shsel2  22015  hsupss  22034  pjhth  22086  shlub  22107  cm2j  22313  lnfncnbd  22751  riesz1  22759  rnbra  22801  leopadd  22826  leopmuli  22827  hstles  22925  stge1i  22932  stle0i  22933  dmdbr5  23002  ssmd2  23006  superpos  23048  chcv1  23049  atoml2i  23077  chirredlem2  23085  atcvat3i  23090  mdsymlem5  23101  mdsymlem6  23102  sumdmdii  23109  sumdmdlem2  23113  iscnp4  23447  sqsscirc2  23463  cnre2csqlem  23464  xrge0iifiso  23477  sigaclci  23781  ballotlemimin  24012  ballotlem7  24042  cvmlift2lem12  24249  dfon2lem8  24704  soseq  24812  axeuclid  25150  segconeq  25192  ifscgr  25226  brofs2  25259  brifs2  25260  endofsegid  25267  fzmul  25767  fdc  25779  incsequz2  25783  sstotbnd2  25821  sstotbnd3  25823  totbndbnd  25836  ispridl2  25986  irrapxlem2  26231  pell14qrdich  26277  monotoddzz  26351  pw2f1ocnv  26453  stoweidlem62  27134  hash2prb  27477  umisuhgra  27514  uslisumgra  27541  usisuslgra  27542  constr3trl  27783  constr3pth  27784  vdusgraval  27814  vdusgrav  27815  sbcim2g  28047  lsator0sp  29260  lssatle  29274  lshpset2N  29378  lkrlspeqN  29430  omllaw2N  29503  cmtbr3N  29513  lecmtN  29515  cvlcvr1  29598  cvrval4N  29672  cvrat3  29700  3noncolr2  29707  4noncolr3  29711  3dimlem3  29719  3dimlem3OLDN  29720  3dimlem4  29722  3dimlem4OLDN  29723  llncvrlpln  29816  lplncvrlvol  29874  snatpsubN  30008  linepsubN  30010  pmapjat1  30111  pclfinclN  30208  pl42N  30241  ltrneq2  30406  cdleme7aa  30500  cdleme18d  30553  cdleme21b  30584  trlord  30827  trlcoat  30981  dochkrshp  31645  lcfl8  31761
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 177
  Copyright terms: Public domain W3C validator