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

Theorem sylbird 250
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 238 . 2 (𝜑 → (𝜓𝜒))
3 sylbird.2 . 2 (𝜑 → (𝜒𝜃))
42, 3syld 47 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  3imtr3d  282  ceqex  3364  eqreu  3431  sotr2  5093  sossfld  5615  ordtr3OLD  5808  ordintdif  5812  tz6.12i  6252  f1cofveqaeqALT  6556  soisoi  6618  riotaeqimp  6674  ov3  6839  tfindsg  7102  tfindsg2  7103  nnsuc  7124  findsg  7135  suppssr  7371  tfrlem9  7526  oe0lem  7638  oa00  7684  omwordi  7696  om00  7700  omass  7705  oelim2  7720  oeoa  7722  oeoe  7724  nnmwordi  7760  swoso  7820  dom2lem  8037  onsdominel  8150  f1finf1o  8228  cantnfp1lem3  8615  cantnfp1  8616  cantnflem1  8624  rankr1ai  8699  rankval3b  8727  harcard  8842  infxpenlem  8874  alephnbtwn  8932  alephinit  8956  infxp  9075  cofsmo  9129  infpssALT  9173  fin23lem24  9182  fin56  9253  ttukeylem6  9374  ficard  9425  alephval2  9432  fpwwe2lem8  9497  fpwwe2  9503  gchcda1  9516  pwfseqlem3  9520  pwfseqlem4a  9521  pwfseqlem4  9522  gchpwdom  9530  tskss  9618  inar1  9635  gruss  9656  gruurn  9658  ltsonq  9829  distrlem4pr  9886  sqgt0sr  9965  map2psrpr  9969  letric  10175  renegcli  10380  addid0  10488  mulge0b  10931  nnge1  11084  0mnnnnn0  11363  nn0lt2  11478  zneo  11498  uzind2  11508  fzind  11513  nn0ind-raph  11515  uzwo  11789  nn01to3  11819  zbtwnre  11824  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  ledivge1le  11939  xrletri  12022  qsqueeze  12070  difreicc  12342  elfzmlbp  12489  difelfznle  12492  elfzodifsumelfzo  12573  ssfzo12  12601  elfzonelfzo  12610  flflp1  12648  fleqceilz  12693  modsumfzodifsn  12783  addmodlteq  12785  om2uzf1oi  12792  facdiv  13114  facwordi  13116  bcpasc  13148  hashdom  13206  hashdmpropge2  13303  ccatsymb  13400  swrdsbslen  13494  swrdspsleq  13495  swrdlsw  13498  swrdswrdlem  13505  swrdccatin1  13529  swrdccatin12lem3  13536  repswswrd  13577  cshwidx0  13598  cshwcsh2id  13620  limsupbnd1  14257  lo1bdd2  14299  addcn2  14368  mulcn2  14370  o1rlimmul  14393  lo1add  14401  lo1mul  14402  rlimno1  14428  znnenlem  14984  ruclem3  15006  odd2np1  15112  oddge22np1  15120  bitsfzo  15204  cncongr1  15428  prm23ge5  15567  pcdvdsb  15620  pcaddlem  15639  infpnlem1  15661  prmunb  15665  vdwlem9  15740  vdwnnlem3  15748  ramcl  15780  prmgaplem5  15806  cshwshash  15858  setcmon  16784  setcepi  16785  setciso  16788  ghmf1  17736  sylow2alem2  18079  sylow2blem3  18083  qusabl  18314  lt6abl  18342  cyggexb  18346  gsumcom2  18420  imasring  18665  f1rhm0to0  18788  drnginvrcl  18812  drnginvrl  18814  drnginvrr  18815  subrgdvds  18842  lsmelval2  19133  quscrng  19288  mplsubrglem  19487  gsummoncoe1  19722  xrsdsreclblem  19840  obs2ss  20121  obslbs  20122  mp2pm2mplem4  20662  chfacfisf  20707  chfacfisfcpmat  20708  cayleyhamilton1  20745  cmpsublem  21250  cmpsub  21251  1stccnp  21313  locfincf  21382  txhaus  21498  xkohaus  21504  ufilss  21756  cfinufil  21779  fmfnfmlem1  21805  hausflim  21832  fclscf  21876  alexsubb  21897  qustgplem  21971  prdsbl  22343  metss2lem  22363  nghmcn  22596  cfil3i  23113  cmetcaulem  23132  minveclem4  23249  ovolgelb  23294  ovolunnul  23314  ovoliun  23319  ovoliunnul  23321  ovolicc2lem2  23332  iundisj2  23363  voliunlem3  23366  rolle  23798  dvlip  23801  lhop1lem  23821  lhop2  23823  dvfsumrlim  23839  deg1ge  23903  coeeulem  24025  dgrco  24076  radcnvlt1  24217  psercnlem1  24224  logcnlem2  24434  logcnlem3  24435  cxpeq  24543  angpined  24602  efrlim  24741  dmgmaddn0  24794  lgamucov  24809  basellem2  24853  ppieq0  24947  mumullem2  24951  chpeq0  24978  chteq0  24979  chtub  24982  fsumvma  24983  dchrptlem1  25034  bposlem6  25059  gausslemma2dlem0i  25134  gausslemma2dlem1a  25135  lgseisenlem2  25146  2sqlem6  25193  dchrisum0lem1  25250  pntrsumbnd2  25301  pntlem3  25343  colinearalg  25835  eengtrkg  25910  incistruhgr  26019  wlkv0  26603  crctcshwlkn0  26769  clwlkclwwlklem2a4  26963  clwlkclwwlklem2  26966  eucrctshift  27221  frrusgrord0  27320  frgrreg  27381  blocni  27788  ubthlem1  27854  minvecolem4  27864  shmodsi  28376  atcvati  29373  atcvat2i  29374  chirredlem4  29380  atmd2  29387  sumdmdlem  29405  addltmulALT  29433  iundisj2f  29529  iundisj2fi  29684  rngurd  29916  erdszelem9  31307  sotr3  31782  rdgprc  31824  soseq  31879  noextenddif  31946  nosupno  31974  nosupbnd1  31985  noetalem3  31990  scutun12  32042  slerec  32048  cgrsub  32277  btwnxfr  32288  lineext  32308  linecgr  32313  btwnconn1lem4  32322  btwnconn1lem5  32323  btwnconn1lem6  32324  btwnconn1lem8  32326  btwnconn1lem11  32329  mptsnunlem  33315  finxpreclem6  33363  ltflcei  33527  poimirlem23  33562  poimirlem24  33563  poimirlem31  33570  poimirlem32  33571  ftc1anclem5  33619  heiborlem6  33745  grpokerinj  33822  dvrunz  33883  isdmn3  34003  dmncan1  34005  l1cvpat  34659  atnle  34922  cvlexch3  34937  cvlexch4N  34938  cvlatexchb1  34939  cvrat2  35033  atlelt  35042  3dimlem4a  35067  3dimlem4OLDN  35069  ps-1  35081  ps-2  35082  4atlem10  35210  4atlem11  35213  4atlem12  35216  cdleme11c  35866  cdleme21c  35932  cdlemg6d  36226  trlcoat  36328  tendoid0  36430  cdleml3N  36583  dia2dimlem7  36676  pellexlem1  37710  pellexlem6  37715  imasgim  37987  iunrelexpmin1  38317  iunrelexpmin2  38321  radcnvrat  38830  nzss  38833  elprneb  41620  zm1nn  41641  2ffzoeq  41663  pfxccat3a  41754  sfprmdvdsmersenne  41845  lighneallem3  41849  lighneallem4  41852  stgoldbwt  41989  sbgoldbaltlem1  41992  lmod0rng  42193  0ring1eq0  42197  lidldomn1  42246  rngciso  42307  rngcisoALTV  42319  ringciso  42358  ringcisoALTV  42382  ztprmneprm  42450  lincresunit3  42595  aacllem  42875
  Copyright terms: Public domain W3C validator