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  3238  eqsbc3r  3269  ordtr2  4784  elreldm  5085  ssimaex  5777  fconstfv  5961  fliftfun  6026  isopolem  6057  isosolem  6059  ordsucss  6450  f1oweALT  6582  fnse  6710  brtpos  6775  issmo2  6831  seqomlem1  6926  omcl  6997  oecl  6998  oawordeulem  7014  oaass  7021  omordi  7026  omord  7028  odi  7039  oen0  7046  oeordi  7047  oeordsuc  7054  nnmcl  7072  nnecl  7073  nnmordi  7091  nnmord  7092  nnmwordri  7096  nnaordex  7098  swoord1  7151  ecopovtrn  7224  f1domg  7350  pw2f1olem  7436  domtriord  7478  mapen  7496  mapxpen  7498  mapunen  7501  nndomo  7525  inficl  7696  supmo  7723  inf3lem6  7860  cantnflem1  7918  cantnflem1OLD  7941  tcmin  7982  tcrank  8112  cardne  8156  cardlim  8163  cardsdomel  8165  carduni  8172  alephord  8266  cardinfima  8288  dfac5lem4  8317  infdif2  8400  cofsmo  8459  cfcoflem  8462  infpssrlem4  8496  infpssrlem5  8497  fin4en1  8499  isfin2-2  8509  enfin2i  8511  fin23lem27  8518  isf32lem12  8554  isf34lem6  8570  domtriomlem  8632  cardmin  8749  fpwwe2lem12  8829  inar1  8963  gruiun  8987  ltsonq  9159  prub  9184  reclem3pr  9239  mulcmpblnr  9262  mulgt0sr  9293  axpre-sup  9357  leltadd  9844  infm3  10310  peano5nni  10346  zextle  10736  prime  10743  uzindOLD  10757  uzin  10914  ublbneg  10960  zbtwnre  10972  xrre2  11163  xralrple  11196  xmulneg1  11253  supxrbnd  11312  supxrgtmnf  11313  fzrevral  11565  flge  11676  ceile  11709  modadd1  11766  modmul1  11773  seqcl2  11845  facdiv  12084  hashss  12187  hash2prb  12201  elfzelfzccat  12300  repswswrd  12443  rlim2lt  12996  rlim3  12997  o1lo1  13036  climshftlem  13073  o1co  13085  o1of2  13111  isercolllem2  13164  isercoll  13166  caucvgrlem2  13173  climcndslem2  13334  sqr2irr  13552  dvds2lem  13566  dvdsle  13599  dvdsfac  13609  divalglem0  13618  ndvdsadd  13633  bitsinv1lem  13658  sadcaddlem  13674  dvdslegcd  13721  bezoutlem2  13744  bezoutlem4  13746  gcdeq  13757  algcvga  13775  prmind2  13795  isprm6  13816  rpexp  13827  rpdvds  13831  eulerthlem2  13878  pclem  13926  pceulem  13933  pc2dvds  13966  fldivp1  13980  infpnlem1  13992  prmunb  13996  mrieqv2d  14598  plttr  15161  clatl  15307  issubg4  15721  gexdvds  16104  pgpssslw  16134  sylow2alem2  16138  efgs1b  16254  efgsfo  16257  lspindpi  17235  pf1ind  17811  psgnodpm  18040  psgndif  18054  obselocv  18175  mdetunilem9  18448  fiinbas  18579  bastg  18593  tgcl  18596  opnssneib  18741  clslp  18774  tgcnp  18879  iscnp4  18889  cncls2  18899  cncls  18900  cnntr  18901  cnpresti  18914  lmss  18924  lmcnp  18930  cmpsub  19025  tgcmp  19026  dfcon2  19045  t1conperf  19062  1stcfb  19071  1stcrest  19079  kgenss  19138  llycmpkgen2  19145  txdis  19227  qtoptop2  19294  kqt0lem  19331  isr0  19332  regr1lem2  19335  cmphaushmeo  19395  fbun  19435  ssfg  19467  fgtr  19485  ufildr  19526  cnpflf  19596  fclsnei  19614  flimfnfcls  19623  fclscmp  19625  ufilcmp  19627  cnpfcf  19636  alexsublem  19638  alexsubALTlem3  19643  alexsubALTlem4  19644  ptcmplem3  19648  tgphaus  19709  tgpt1  19710  tsmsresOLD  19739  tsmsres  19740  imasdsf1olem  19970  xblss2ps  19998  xblss2  19999  blsscls2  20101  metequiv2  20107  stdbdxmet  20112  nmoi  20329  reconn  20427  mulc1cncf  20503  cncfco  20505  iccpnfhmeo  20539  xrhmeo  20540  evth  20553  pi1grplem  20643  fgcfil  20804  ivthlem2  20958  ivthlem3  20959  ovolicc2lem4  21025  voliunlem1  21053  ioombl1lem4  21064  itg2gt0  21260  limcco  21390  lhop1  21508  tdeglem4  21551  plypf1  21702  coeeulem  21714  coeidlem  21727  coeid3  21730  plymul0or  21769  dvnply2  21775  plydivex  21785  vieta1lem2  21799  plyexmo  21801  aaliou3lem2  21831  ulmss  21884  ulmdvlem3  21889  iblulm  21894  sincosq2sgn  21983  sincosq3sgn  21984  sincosq4sgn  21985  logcnlem5  22113  dcubic  22263  amgm  22406  isnsqf  22495  mumullem2  22540  chtublem  22572  chtub  22573  fsumvma2  22575  vmasum  22577  dchrfi  22616  bposlem1  22645  bposlem3  22647  bposlem7  22651  lgsdir  22691  lgsquadlem2  22716  2sqlem8a  22732  2sqlem10  22735  dchrisum0flb  22781  pntpbnd1  22857  pntlemf  22876  pntlem3  22880  axeuclid  23231  umisuhgra  23283  uslisumgra  23307  usisuslgra  23308  constr3trl  23567  constr3pth  23568  vdusgraval  23599  gxcl  23774  isexid2  23834  lnon0  24220  normpyc  24570  ocsh  24708  ocorth  24716  ococss  24718  shsel2  24747  hsupss  24766  pjhth  24818  shlub  24839  cm2j  25045  lnfncnbd  25483  riesz1  25491  rnbra  25533  leopadd  25558  leopmuli  25559  hstles  25657  stge1i  25664  stle0i  25665  dmdbr5  25734  ssmd2  25738  superpos  25780  chcv1  25781  atoml2i  25809  chirredlem2  25817  atcvat3i  25822  mdsymlem5  25833  mdsymlem6  25834  sumdmdii  25841  sumdmdlem2  25845  mul2lt0bi  26064  isarchiofld  26307  sqsscirc2  26361  cnre2csqlem  26362  xrge0iifiso  26387  sigaclci  26597  eulerpartlemb  26773  ballotlemimin  26910  ballotlem7  26940  cvmlift2lem12  27225  dfon2lem8  27625  soseq  27737  segconeq  28063  ifscgr  28097  brofs2  28130  brifs2  28131  endofsegid  28138  tan2h  28450  fzmul  28662  fdc  28667  incsequz2  28671  sstotbnd2  28699  sstotbnd3  28701  totbndbnd  28714  ispridl2  28864  mpt2bi123f  29001  irrapxlem2  29190  pell14qrdich  29236  monotoddzz  29310  pw2f1ocnv  29412  iocinico  29613  stoweidlem62  29883  elfzelfzlble  30235  wwlknext  30382  wwlkextsur  30389  clwwisshclwwlem1  30495  erclwwlktr0  30505  sbcim2g  31341  riotasvd  32703  lsator0sp  32742  lssatle  32756  lshpset2N  32860  lkrlspeqN  32912  omllaw2N  32985  cmtbr3N  32995  lecmtN  32997  cvlcvr1  33080  cvrval4N  33154  cvrat3  33182  3noncolr2  33189  4noncolr3  33193  3dimlem3  33201  3dimlem3OLDN  33202  3dimlem4  33204  3dimlem4OLDN  33205  llncvrlpln  33298  lplncvrlvol  33356  snatpsubN  33490  linepsubN  33492  pmapjat1  33593  pclfinclN  33690  pl42N  33723  ltrneq2  33888  cdleme7aa  33982  cdleme18d  34035  cdleme21b  34066  trlord  34309  trlcoat  34463  dochkrshp  35127  lcfl8  35243
  Copyright terms: Public domain W3C validator