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

Theorem sylbird 251
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 239 . 2 (𝜑 → (𝜓𝜒))
3 sylbird.2 . 2 (𝜑 → (𝜒𝜃))
42, 3syld 47 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  3imtr3d  284  ceqex  3526  eqreu  3593  sotr2  5258  sossfld  5788  ordtr3OLD  5980  ordintdif  5984  tz6.12i  6431  f1cofveqaeqALT  6737  soisoi  6799  riotaeqimp  6855  ov3  7024  tfindsg  7287  tfindsg2  7288  nnsuc  7309  findsg  7320  suppssr  7558  tfrlem9  7714  oe0lem  7827  oa00  7873  omwordi  7885  om00  7889  omass  7894  oelim2  7909  oeoa  7911  oeoe  7913  nnmwordi  7949  swoso  8009  dom2lem  8229  onsdominel  8345  f1finf1o  8423  cantnfp1lem3  8821  cantnfp1  8822  cantnflem1  8830  rankr1ai  8905  rankval3b  8933  harcard  9084  infxpenlem  9116  alephnbtwn  9174  alephinit  9198  infxp  9319  cofsmo  9373  infpssALT  9417  fin23lem24  9426  fin56  9497  ttukeylem6  9618  ficard  9669  alephval2  9676  fpwwe2lem8  9741  fpwwe2  9747  gchcda1  9760  pwfseqlem3  9764  pwfseqlem4a  9765  pwfseqlem4  9766  gchpwdom  9774  tskss  9862  inar1  9879  gruss  9900  gruurn  9902  ltsonq  10073  distrlem4pr  10130  sqgt0sr  10209  map2psrpr  10213  letric  10419  renegcli  10624  addid0  10732  mulge0b  11175  nnge1  11328  0mnnnnn0  11587  nn0lt2  11702  zneo  11722  uzind2  11732  fzind  11737  nn0ind-raph  11739  uzwo  11966  nn01to3  11996  zbtwnre  12001  rpnnen1lem5  12033  ledivge1le  12111  xrletri  12198  qsqueeze  12246  difreicc  12523  elfzmlbp  12670  difelfznle  12673  elfzodifsumelfzo  12754  ssfzo12  12781  elfzonelfzo  12790  flflp1  12828  fleqceilz  12873  modsumfzodifsn  12963  addmodlteq  12965  om2uzf1oi  12972  facdiv  13290  facwordi  13292  bcpasc  13324  hashdom  13382  hashdmpropge2  13478  ccatsymb  13575  swrdsbslen  13668  swrdspsleq  13669  swrdlsw  13672  swrdswrdlem  13679  swrdccatin1  13703  swrdccatin12lem3  13710  repswswrd  13751  cshwidx0  13772  cshwcsh2id  13794  limsupbnd1  14432  lo1bdd2  14474  addcn2  14543  mulcn2  14545  o1rlimmul  14568  lo1add  14576  lo1mul  14577  rlimno1  14603  znnenlemOLD  15156  ruclem3  15178  odd2np1  15281  oddge22np1  15289  bitsfzo  15372  cncongr1  15595  prm23ge5  15733  pcdvdsb  15786  pcaddlem  15805  infpnlem1  15827  prmunb  15831  vdwlem9  15906  vdwnnlem3  15914  ramcl  15946  prmgaplem5  15972  cshwshash  16019  setcmon  16937  setcepi  16938  setciso  16941  ghmf1  17887  sylow2alem2  18230  sylow2blem3  18234  qusabl  18465  lt6abl  18493  cyggexb  18497  gsumcom2  18571  imasring  18817  f1rhm0to0  18940  drnginvrcl  18964  drnginvrl  18966  drnginvrr  18967  subrgdvds  18994  lsmelval2  19288  quscrng  19445  mplsubrglem  19644  gsummoncoe1  19878  xrsdsreclblem  19996  obs2ss  20279  obslbs  20280  mp2pm2mplem4  20823  chfacfisf  20868  chfacfisfcpmat  20869  cayleyhamilton1  20906  cmpsublem  21412  cmpsub  21413  1stccnp  21475  locfincf  21544  txhaus  21660  xkohaus  21666  ufilss  21918  cfinufil  21941  fmfnfmlem1  21967  hausflim  21994  fclscf  22038  alexsubb  22059  qustgplem  22133  prdsbl  22505  metss2lem  22525  nghmcn  22758  cfil3i  23275  cmetcaulem  23294  minveclem4  23411  ovolgelb  23457  ovolunnul  23477  ovoliun  23482  ovoliunnul  23484  ovolicc2lem2  23495  iundisj2  23526  voliunlem3  23529  rolle  23963  dvlip  23966  lhop1lem  23986  lhop2  23988  dvfsumrlim  24004  deg1ge  24068  coeeulem  24190  dgrco  24241  radcnvlt1  24382  psercnlem1  24389  logcnlem2  24599  logcnlem3  24600  cxpeq  24708  angpined  24767  efrlim  24906  dmgmaddn0  24959  lgamucov  24974  basellem2  25018  ppieq0  25112  mumullem2  25116  chpeq0  25143  chteq0  25144  chtub  25147  fsumvma  25148  dchrptlem1  25199  bposlem6  25224  gausslemma2dlem0i  25299  gausslemma2dlem1a  25300  lgseisenlem2  25311  2sqlem6  25358  dchrisum0lem1  25415  pntrsumbnd2  25466  pntlem3  25508  colinearalg  26000  eengtrkg  26075  incistruhgr  26184  wlkv0  26771  crctcshwlkn0  26938  clwlkclwwlklem2a4  27136  clwlkclwwlklem2  27139  clwlkclwwlkfo  27148  eucrctshift  27412  frrusgrord0  27511  frgrreg  27578  blocni  27985  ubthlem1  28051  minvecolem4  28061  shmodsi  28573  atcvati  29570  atcvat2i  29571  chirredlem4  29577  atmd2  29584  sumdmdlem  29602  addltmulALT  29630  iundisj2f  29725  iundisj2fi  29880  rngurd  30110  erdszelem9  31501  sotr3  31975  rdgprc  32017  soseq  32072  noextenddif  32139  nosupno  32167  nosupbnd1  32178  noetalem3  32183  scutun12  32235  slerec  32241  cgrsub  32470  btwnxfr  32481  lineext  32501  linecgr  32506  btwnconn1lem4  32515  btwnconn1lem5  32516  btwnconn1lem6  32517  btwnconn1lem8  32519  btwnconn1lem11  32522  mptsnunlem  33499  finxpreclem6  33546  ltflcei  33707  poimirlem23  33742  poimirlem24  33743  poimirlem31  33750  poimirlem32  33751  ftc1anclem5  33798  heiborlem6  33923  grpokerinj  34000  dvrunz  34061  isdmn3  34181  dmncan1  34183  l1cvpat  34831  atnle  35094  cvlexch3  35109  cvlexch4N  35110  cvlatexchb1  35111  cvrat2  35206  atlelt  35215  3dimlem4a  35240  3dimlem4OLDN  35242  ps-1  35254  ps-2  35255  4atlem10  35383  4atlem11  35386  4atlem12  35389  cdleme11c  36039  cdleme21c  36105  cdlemg6d  36399  trlcoat  36501  tendoid0  36603  cdleml3N  36756  dia2dimlem7  36848  pellexlem1  37892  pellexlem6  37897  imasgim  38168  iunrelexpmin1  38497  iunrelexpmin2  38501  radcnvrat  39010  nzss  39013  elprneb  41650  tz6.12i-afv2  41829  dfatcolem  41841  f1oresf1o2  41878  zm1nn  41889  2ffzoeq  41910  pfxccat3a  42001  sfprmdvdsmersenne  42092  lighneallem3  42096  lighneallem4  42099  stgoldbwt  42236  sbgoldbaltlem1  42239  lmod0rng  42433  0ring1eq0  42437  lidldomn1  42486  rngciso  42547  rngcisoALTV  42559  ringciso  42598  ringcisoALTV  42622  ztprmneprm  42690  lincresunit3  42835  aacllem  43115
  Copyright terms: Public domain W3C validator