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

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

Proof of Theorem sylbird
StepHypRef Expression
1 sylbird.1 . . 3 (𝜑 → (𝜒𝜓))
21biimprd 237 . 2 (𝜑 → (𝜓𝜒))
3 sylbird.2 . 2 (𝜑 → (𝜒𝜃))
42, 3syld 46 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  3imtr3d  281  ceqex  3303  eqreu  3365  sotr2  4988  sossfld  5499  ordtr3OLD  5687  ordintdif  5691  tz6.12i  6124  soisoi  6478  ov3  6695  tfindsg  6952  tfindsg2  6953  nnsuc  6974  findsg  6985  suppssr  7213  tfrlem9  7368  oe0lem  7480  oa00  7526  omwordi  7538  om00  7542  omass  7547  oelim2  7562  oeoa  7564  oeoe  7566  nnmwordi  7602  swoso  7662  dom2lem  7881  onsdominel  7994  f1finf1o  8072  cantnfp1lem3  8460  cantnfp1  8461  cantnflem1  8469  rankr1ai  8544  rankval3b  8572  harcard  8687  infxpenlem  8719  alephnbtwn  8777  alephinit  8801  infxp  8920  cofsmo  8974  infpssALT  9018  fin23lem24  9027  fin56  9098  ttukeylem6  9219  ficard  9266  alephval2  9273  fpwwe2lem8  9338  fpwwe2  9344  gchcda1  9357  pwfseqlem3  9361  pwfseqlem4a  9362  pwfseqlem4  9363  gchpwdom  9371  tskss  9459  inar1  9476  gruss  9497  gruurn  9499  ltsonq  9670  distrlem4pr  9727  sqgt0sr  9806  map2psrpr  9810  letric  10016  renegcli  10221  addid0  10329  mulge0b  10772  nnge1  10923  0mnnnnn0  11202  nn0lt2  11317  zneo  11336  uzind2  11346  fzind  11351  nn0ind-raph  11353  uzwo  11627  nn01to3  11657  zbtwnre  11662  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  ledivge1le  11777  xrletri  11860  qsqueeze  11906  difreicc  12175  elfzmlbp  12319  difelfznle  12322  elfzodifsumelfzo  12401  ssfzo12  12427  elfzonelfzo  12436  flflp1  12470  fleqceilz  12515  modsumfzodifsn  12605  addmodlteq  12607  om2uzf1oi  12614  facdiv  12936  facwordi  12938  bcpasc  12970  hashdom  13029  ccatsymb  13219  swrdsbslen  13300  swrdspsleq  13301  swrdlsw  13304  swrdswrdlem  13311  swrdccatin1  13334  swrdccatin12lem3  13341  repswswrd  13382  cshwidx0  13403  cshwcsh2id  13425  limsupbnd1  14061  lo1bdd2  14103  addcn2  14172  mulcn2  14174  o1rlimmul  14197  lo1add  14205  lo1mul  14206  rlimno1  14232  znnenlem  14779  ruclem3  14801  odd2np1  14903  oddge22np1  14911  bitsfzo  14995  cncongr1  15219  prm23ge5  15358  pcdvdsb  15411  pcaddlem  15430  infpnlem1  15452  prmunb  15456  vdwlem9  15531  vdwnnlem3  15539  ramcl  15571  prmgaplem5  15597  cshwshash  15649  setcmon  16560  setcepi  16561  setciso  16564  ghmf1  17512  sylow2alem2  17856  sylow2blem3  17860  qusabl  18091  lt6abl  18119  cyggexb  18123  gsumcom2  18197  imasring  18442  f1rhm0to0  18563  drnginvrcl  18587  drnginvrl  18589  drnginvrr  18590  subrgdvds  18617  lsmelval2  18906  quscrng  19061  mplsubrglem  19260  gsummoncoe1  19495  xrsdsreclblem  19611  obs2ss  19892  obslbs  19893  mp2pm2mplem4  20433  chfacfisf  20478  chfacfisfcpmat  20479  cayleyhamilton1  20516  cmpsublem  21012  cmpsub  21013  1stccnp  21075  locfincf  21144  txhaus  21260  xkohaus  21266  ufilss  21519  cfinufil  21542  fmfnfmlem1  21568  hausflim  21595  fclscf  21639  alexsubb  21660  qustgplem  21734  prdsbl  22106  metss2lem  22126  nghmcn  22359  cfil3i  22875  cmetcaulem  22894  minveclem4  23011  ovolgelb  23055  ovolunnul  23075  ovoliun  23080  ovoliunnul  23082  ovolicc2lem2  23093  iundisj2  23124  voliunlem3  23127  rolle  23557  dvlip  23560  lhop1lem  23580  lhop2  23582  dvfsumrlim  23598  deg1ge  23662  coeeulem  23784  dgrco  23835  radcnvlt1  23976  psercnlem1  23983  logcnlem2  24189  logcnlem3  24190  cxpeq  24298  angpined  24357  efrlim  24496  dmgmaddn0  24549  lgamucov  24564  basellem2  24608  ppieq0  24702  mumullem2  24706  chpeq0  24733  chteq0  24734  chtub  24737  fsumvma  24738  dchrptlem1  24789  bposlem6  24814  gausslemma2dlem0i  24889  gausslemma2dlem1a  24890  lgseisenlem2  24901  2sqlem6  24948  dchrisum0lem1  25005  pntrsumbnd2  25056  pntlem3  25098  colinearalg  25590  eengtrkg  25665  incistruhgr  25746  wlkv0  26288  0clwlk  26293  clwwlkgt0  26299  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem1  26315  nbhashuvtx1  26442  blocni  27044  ubthlem1  27110  minvecolem4  27120  shmodsi  27632  atcvati  28629  atcvat2i  28630  chirredlem4  28636  atmd2  28643  sumdmdlem  28661  addltmulALT  28689  iundisj2f  28785  iundisj2fi  28943  rngurd  29119  erdszelem9  30435  rdgprc  30944  soseq  30995  cgrsub  31322  btwnxfr  31333  lineext  31353  linecgr  31358  btwnconn1lem4  31367  btwnconn1lem5  31368  btwnconn1lem6  31369  btwnconn1lem8  31371  btwnconn1lem11  31374  mptsnunlem  32361  finxpreclem6  32409  ltflcei  32567  poimirlem23  32602  poimirlem24  32603  poimirlem31  32610  poimirlem32  32611  ftc1anclem5  32659  heiborlem6  32785  grpokerinj  32862  dvrunz  32923  isdmn3  33043  dmncan1  33045  l1cvpat  33359  atnle  33622  cvlexch3  33637  cvlexch4N  33638  cvlatexchb1  33639  cvrat2  33733  atlelt  33742  3dimlem4a  33767  3dimlem4OLDN  33769  ps-1  33781  ps-2  33782  4atlem10  33910  4atlem11  33913  4atlem12  33916  cdleme11c  34566  cdleme21c  34633  cdlemg6d  34927  trlcoat  35029  tendoid0  35131  cdleml3N  35284  dia2dimlem7  35377  pellexlem1  36411  pellexlem6  36416  imasgim  36688  iunrelexpmin1  37019  iunrelexpmin2  37023  radcnvrat  37535  nzss  37538  elprneb  39939  sfprmdvdsmersenne  40058  lighneallem3  40062  lighneallem4  40065  stgoldbwt  40198  sgoldbaltlem1  40201  pfxccat3a  40292  f1cofveqaeqALT  40324  riotaeqimp  40338  zm1nn  40348  2ffzoeq  40361  1wlkv0  40859  crctcsh1wlkn0  41024  clwlkclwwlklem2a4  41206  clwlkclwwlklem2  41209  eucrctshift  41411  av-frgrareg  41548  lmod0rng  41658  0ring1eq0  41662  lidldomn1  41711  rngciso  41774  rngcisoALTV  41786  ringciso  41825  ringcisoALTV  41849  ztprmneprm  41918  lincresunit3  42064  aacllem  42356
  Copyright terms: Public domain W3C validator