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

Theorem sylbird 248
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 236 . 2 (𝜑 → (𝜓𝜒))
3 sylbird.2 . 2 (𝜑 → (𝜒𝜃))
42, 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:  3imtr3d  280  ceqex  3302  eqreu  3364  sotr2  4977  sossfld  5484  ordtr3OLD  5672  ordintdif  5676  tz6.12i  6108  soisoi  6455  ov3  6672  tfindsg  6929  tfindsg2  6930  nnsuc  6951  findsg  6962  suppssr  7190  tfrlem9  7345  oe0lem  7457  oa00  7503  omwordi  7515  om00  7519  omass  7524  oelim2  7539  oeoa  7541  oeoe  7543  nnmwordi  7579  swoso  7639  dom2lem  7858  onsdominel  7971  f1finf1o  8049  cantnfp1lem3  8437  cantnfp1  8438  cantnflem1  8446  rankr1ai  8521  rankval3b  8549  harcard  8664  infxpenlem  8696  alephnbtwn  8754  alephinit  8778  infxp  8897  cofsmo  8951  infpssALT  8995  fin23lem24  9004  fin56  9075  ttukeylem6  9196  ficard  9243  alephval2  9250  fpwwe2lem8  9315  fpwwe2  9321  gchcda1  9334  pwfseqlem3  9338  pwfseqlem4a  9339  pwfseqlem4  9340  gchpwdom  9348  tskss  9436  inar1  9453  gruss  9474  gruurn  9476  ltsonq  9647  distrlem4pr  9704  sqgt0sr  9783  map2psrpr  9787  letric  9988  renegcli  10193  addid0  10301  mulge0b  10744  nnge1  10895  0mnnnnn0  11174  nn0lt2  11275  zneo  11294  uzind2  11304  fzind  11309  nn0ind-raph  11311  uzwo  11585  nn01to3  11615  zbtwnre  11620  rpnnen1lem5  11652  rpnnen1lem5OLD  11658  ledivge1le  11735  xrletri  11821  qsqueeze  11867  difreicc  12133  elfzmlbp  12276  difelfznle  12279  elfzodifsumelfzo  12358  ssfzo12  12384  elfzonelfzo  12393  flflp1  12427  fleqceilz  12472  modsumfzodifsn  12562  addmodlteq  12564  om2uzf1oi  12571  facdiv  12893  facwordi  12895  bcpasc  12927  hashdom  12983  hashle00  13003  ccatsymb  13167  swrdsbslen  13248  swrdspsleq  13249  swrdlsw  13252  swrdswrdlem  13259  swrdccatin1  13282  swrdccatin12lem3  13289  repswswrd  13330  cshwidx0  13351  cshwcsh2id  13373  limsupbnd1  14009  lo1bdd2  14051  addcn2  14120  mulcn2  14122  o1rlimmul  14145  lo1add  14153  lo1mul  14154  rlimno1  14180  znnenlem  14727  ruclem3  14749  odd2np1  14851  oddge22np1  14859  bitsfzo  14943  cncongr1  15167  prm23ge5  15306  pcdvdsb  15359  pcaddlem  15378  infpnlem1  15400  prmunb  15404  vdwlem9  15479  vdwnnlem3  15487  ramcl  15519  prmgaplem5  15545  cshwshash  15597  setcmon  16508  setcepi  16509  setciso  16512  ghmf1  17460  sylow2alem2  17804  sylow2blem3  17808  qusabl  18039  lt6abl  18067  cyggexb  18071  gsumcom2  18145  imasring  18390  f1rhm0to0  18511  drnginvrcl  18535  drnginvrl  18537  drnginvrr  18538  subrgdvds  18565  lsmelval2  18854  quscrng  19009  mplsubrglem  19208  gsummoncoe1  19443  xrsdsreclblem  19559  obs2ss  19839  obslbs  19840  mp2pm2mplem4  20380  chfacfisf  20425  chfacfisfcpmat  20426  cayleyhamilton1  20463  cmpsublem  20959  cmpsub  20960  1stccnp  21022  locfincf  21091  txhaus  21207  xkohaus  21213  ufilss  21466  cfinufil  21489  fmfnfmlem1  21515  hausflim  21542  fclscf  21586  alexsubb  21607  qustgplem  21681  prdsbl  22053  metss2lem  22073  nghmcn  22306  cfil3i  22819  cmetcaulem  22838  minveclem4  22955  ovolgelb  22999  ovolunnul  23019  ovoliun  23024  ovoliunnul  23026  ovolicc2lem2  23037  iundisj2  23068  voliunlem3  23071  rolle  23501  dvlip  23504  lhop1lem  23524  lhop2  23526  dvfsumrlim  23542  deg1ge  23606  coeeulem  23728  dgrco  23779  radcnvlt1  23920  psercnlem1  23927  logcnlem2  24133  logcnlem3  24134  cxpeq  24242  angpined  24301  efrlim  24440  dmgmaddn0  24493  lgamucov  24508  basellem2  24552  ppieq0  24646  mumullem2  24650  chpeq0  24677  chteq0  24678  chtub  24681  fsumvma  24682  dchrptlem1  24733  bposlem6  24758  gausslemma2dlem0i  24833  gausslemma2dlem1a  24834  lgseisenlem2  24845  2sqlem6  24892  dchrisum0lem1  24949  pntrsumbnd2  25000  pntlem3  25042  colinearalg  25535  eengtrkg  25610  wlkv0  26081  0clwlk  26086  clwwlkgt0  26092  clwlkisclwwlklem2a4  26105  clwlkisclwwlklem1  26108  nbhashuvtx1  26235  blocni  26837  ubthlem1  26903  minvecolem4  26913  shmodsi  27425  atcvati  28422  atcvat2i  28423  chirredlem4  28429  atmd2  28436  sumdmdlem  28454  addltmulALT  28482  iundisj2f  28578  iundisj2fi  28736  rngurd  28912  erdszelem9  30228  rdgprc  30737  soseq  30788  cgrsub  31115  btwnxfr  31126  lineext  31146  linecgr  31151  btwnconn1lem4  31160  btwnconn1lem5  31161  btwnconn1lem6  31162  btwnconn1lem8  31164  btwnconn1lem11  31167  mptsnunlem  32144  finxpreclem6  32192  ltflcei  32350  poimirlem23  32385  poimirlem24  32386  poimirlem31  32393  poimirlem32  32394  ftc1anclem5  32442  heiborlem6  32568  grpokerinj  32645  dvrunz  32706  isdmn3  32826  dmncan1  32828  l1cvpat  33142  atnle  33405  cvlexch3  33420  cvlexch4N  33421  cvlatexchb1  33422  cvrat2  33516  atlelt  33525  3dimlem4a  33550  3dimlem4OLDN  33552  ps-1  33564  ps-2  33565  4atlem10  33693  4atlem11  33696  4atlem12  33699  cdleme11c  34349  cdleme21c  34416  cdlemg6d  34710  trlcoat  34812  tendoid0  34914  cdleml3N  35067  dia2dimlem7  35160  pellexlem1  36194  pellexlem6  36199  imasgim  36471  iunrelexpmin1  36802  iunrelexpmin2  36806  radcnvrat  37318  nzss  37321  elprneb  39723  sfprmdvdsmersenne  39842  lighneallem3  39846  lighneallem4  39849  stgoldbwt  39982  sgoldbaltlem1  39985  pfxccat3a  40076  f1cofveqaeqALT  40119  riotaeqimp  40144  zm1nn  40154  2ffzoeq  40167  incistruhgr  40286  1wlkv0  40840  crctcsh1wlkn0  41005  clwlkclwwlklem2a4  41187  clwlkclwwlklem2  41190  eucrctshift  41392  av-frgrareg  41529  lmod0rng  41639  0ring1eq0  41643  lidldomn1  41692  rngciso  41755  rngcisoALTV  41767  ringciso  41806  ringcisoALTV  41830  ztprmneprm  41899  lincresunit3  42045  aacllem  42298
  Copyright terms: Public domain W3C validator