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

Theorem sylibrd 247
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylibrd.1 (𝜑 → (𝜓𝜒))
sylibrd.2 (𝜑 → (𝜃𝜒))
Assertion
Ref Expression
sylibrd (𝜑 → (𝜓𝜃))

Proof of Theorem sylibrd
StepHypRef Expression
1 sylibrd.1 . 2 (𝜑 → (𝜓𝜒))
2 sylibrd.2 . . 3 (𝜑 → (𝜃𝜒))
32biimprd 236 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 45 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  3imtr4d  281  sbciegft  3432  eqsbc3rOLD  3459  opeldmd  5236  elreldm  5258  ordtr2  5671  ssimaex  6158  fliftfun  6440  isopolem  6473  isosolem  6475  ordsucss  6888  f1oweALT  7021  fnse  7159  brtpos  7226  issmo2  7311  seqomlem1  7410  omcl  7481  oecl  7482  oawordeulem  7499  oaass  7506  omordi  7511  omord  7513  odi  7524  oen0  7531  oeordi  7532  oeordsuc  7539  nnmcl  7557  nnecl  7558  nnmordi  7576  nnmord  7577  nnmwordri  7581  nnaordex  7583  swoord1  7638  ecopovtrn  7715  f1domg  7839  pw2f1olem  7927  domtriord  7969  mapen  7987  mapxpen  7989  mapunen  7992  nndomo  8017  inficl  8192  supmo  8219  infmo  8262  inf3lem6  8391  cantnflem1  8447  tcmin  8478  tcrank  8608  cardne  8652  cardlim  8659  cardsdomel  8661  carduni  8668  alephord  8759  cardinfima  8781  dfac5lem4  8810  infdif2  8893  cofsmo  8952  cfcoflem  8955  infpssrlem4  8989  infpssrlem5  8990  fin4en1  8992  isfin2-2  9002  enfin2i  9004  fin23lem27  9011  isf32lem12  9047  isf34lem6  9063  domtriomlem  9125  cardmin  9243  fpwwe2lem12  9320  inar1  9454  gruiun  9478  ltsonq  9648  prub  9673  reclem3pr  9728  mulcmpblnr  9749  mulgt0sr  9783  axpre-sup  9847  leltadd  10364  infm3  10834  peano5nni  10873  zextle  11285  prime  11293  uzin  11555  ublbneg  11608  zbtwnre  11621  mul2lt0bi  11771  xrre2  11837  xralrple  11872  xmulneg1  11931  supxrbnd  11989  supxrgtmnf  11990  fzrevral  12252  flge  12426  ceile  12468  modadd1  12527  modmul1  12543  modsumfzodifsn  12563  seqcl2  12639  facdiv  12894  hashss  13013  hash2exprb  13065  elfzelfzccat  13166  repswswrd  13331  cshf1  13356  cshwcsh2id  13374  rlim2lt  14025  rlim3  14026  o1lo1  14065  climshftlem  14102  o1co  14114  o1of2  14140  isercolllem2  14193  isercoll  14195  caucvgrlem2  14202  climcndslem2  14370  sqrt2irr  14766  dvds2lem  14781  dvdsle  14819  dvdsfac  14835  ltoddhalfle  14872  divalglem0  14903  ndvdsadd  14921  bitsinv1lem  14950  sadcaddlem  14966  dvdslegcd  15013  bezoutlem2  15044  bezoutlem4  15046  gcdzeq  15058  algcvga  15079  rpdvds  15161  cncongr1  15168  cncongr2  15169  prmind2  15185  isprm6  15213  rpexp  15219  eulerthlem2  15274  pclem  15330  pceulem  15337  pc2dvds  15370  fldivp1  15388  infpnlem1  15401  prmunb  15405  mrieqv2d  16071  plttr  16742  clatl  16888  issubg4  17385  gexdvds  17771  pgpssslw  17801  sylow2alem2  17805  efgs1b  17921  efgsfo  17924  lspindpi  18902  pf1ind  19489  psgnodpm  19701  psgndif  19715  obselocv  19839  mdetunilem9  20193  fiinbas  20515  bastg  20529  tgcl  20532  opnssneib  20677  clslp  20710  tgcnp  20815  iscnp4  20825  cncls2  20835  cncls  20836  cnntr  20837  cnpresti  20850  lmss  20860  lmcnp  20866  cmpsub  20961  tgcmp  20962  dfcon2  20980  t1conperf  20997  1stcfb  21006  1stcrest  21014  kgenss  21104  llycmpkgen2  21111  txdis  21193  qtoptop2  21260  kqt0lem  21297  isr0  21298  regr1lem2  21301  cmphaushmeo  21361  fbun  21402  ssfg  21434  fgtr  21452  ufildr  21493  cnpflf  21563  fclsnei  21581  flimfnfcls  21590  fclscmp  21592  ufilcmp  21594  cnpfcf  21603  alexsublem  21606  alexsubALTlem3  21611  alexsubALTlem4  21612  ptcmplem3  21616  tgphaus  21678  tgpt1  21679  tsmsres  21705  imasdsf1olem  21936  xblss2ps  21964  xblss2  21965  blsscls2  22067  metequiv2  22073  stdbdxmet  22078  nmoi  22290  reconn  22387  mulc1cncf  22464  cncfco  22466  iccpnfhmeo  22500  xrhmeo  22501  evth  22514  pi1grplem  22605  fgcfil  22822  ivthlem2  22973  ivthlem3  22974  ovolicc2lem4  23040  voliunlem1  23070  ioombl1lem4  23081  itg2gt0  23278  limcco  23408  lhop1  23526  tdeglem4  23569  plypf1  23717  coeeulem  23729  coeidlem  23742  coeid3  23745  plymul0or  23785  dvnply2  23791  plydivex  23801  vieta1lem2  23815  plyexmo  23817  aaliou3lem2  23847  ulmss  23900  ulmdvlem3  23905  iblulm  23910  sincosq2sgn  24000  sincosq3sgn  24001  sincosq4sgn  24002  logcnlem5  24137  dcubic  24318  amgm  24462  isnsqf  24606  mumullem2  24651  chtublem  24681  chtub  24682  fsumvma2  24684  vmasum  24686  dchrfi  24725  bposlem1  24754  bposlem3  24756  bposlem7  24760  lgsdir  24802  lgsquadlem2  24851  2sqlem8a  24895  2sqlem10  24898  dchrisum0flb  24944  pntpbnd1  25020  pntlemf  25039  pntlem3  25043  axeuclid  25589  umisuhgra  25650  uslisushgra  25686  uslisumgra  25687  usisuslgra  25688  constr3trl  25981  constr3pth  25982  wwlknext  26046  wwlkextsur  26053  clwwisshclwwlem1  26127  vdusgraval  26228  lnon0  26871  normpyc  27221  ocsh  27360  ocorth  27368  ococss  27370  shsel2  27399  hsupss  27418  pjhth  27470  shlub  27491  cm2j  27697  lnfncnbd  28134  riesz1  28142  rnbra  28184  leopadd  28209  leopmuli  28210  hstles  28308  stge1i  28315  stle0i  28316  dmdbr5  28385  ssmd2  28389  superpos  28431  chcv1  28432  atoml2i  28460  chirredlem2  28468  atcvat3i  28473  mdsymlem5  28484  mdsymlem6  28485  sumdmdii  28492  sumdmdlem2  28496  isarchiofld  28982  sqsscirc2  29117  cnre2csqlem  29118  xrge0iifiso  29143  sigaclci  29356  omssubadd  29523  eulerpartlemb  29591  ballotlemimin  29728  ballotlem7  29758  cvmlift2lem12  30384  dfon2lem8  30773  soseq  30829  segconeq  31121  ifscgr  31155  brofs2  31188  brifs2  31189  endofsegid  31196  dissneqlem  32187  tan2h  32395  matunitlindflem2  32400  poimirlem31  32434  poimir  32436  fzmul  32531  fdc  32535  incsequz2  32539  sstotbnd2  32567  sstotbnd3  32569  totbndbnd  32582  isexid2  32648  ispridl2  32831  mpt2bi123f  32965  riotasvd  33084  lsator0sp  33130  lssatle  33144  lshpset2N  33248  lkrlspeqN  33300  omllaw2N  33373  cmtbr3N  33383  lecmtN  33385  cvlcvr1  33468  cvrval4N  33542  cvrat3  33570  3noncolr2  33577  4noncolr3  33581  3dimlem3  33589  3dimlem3OLDN  33590  3dimlem4  33592  3dimlem4OLDN  33593  llncvrlpln  33686  lplncvrlvol  33744  snatpsubN  33878  linepsubN  33880  pmapjat1  33981  pclfinclN  34078  pl42N  34111  ltrneq2  34276  cdleme7aa  34371  cdleme18d  34424  cdleme21b  34456  trlord  34699  trlcoat  34853  dochkrshp  35517  lcfl8  35633  irrapxlem2  36229  pell14qrdich  36275  monotoddzz  36350  pw2f1ocnv  36446  iocinico  36640  sbcim2g  37593  stoweidlem62  38779  elfzelfzlble  40205  uspgrushgr  40427  uspgrupgr  40428  usgruspgr  40430  crctcsh1wlkn0lem5  41039  wwlksnext  41121  wwlksnextsur  41128  clwwisshclwwslemlem  41255
  Copyright terms: Public domain W3C validator