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

Theorem sylbird 239
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylbird.1  |-  ( ph  ->  ( ch  <->  ps )
)
sylbird.2  |-  ( ph  ->  ( ch  ->  th )
)
Assertion
Ref Expression
sylbird  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem sylbird
StepHypRef Expression
1 sylbird.1 . . 3  |-  ( ph  ->  ( ch  <->  ps )
)
21biimprd 227 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbird.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 45 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  3imtr3d  271  ceqex  3171  eqreu  3232  sotr2  4787  sossfld  5286  ordtr3  5471  ordintdif  5475  tz6.12i  5890  soisoi  6224  ov3  6438  tfindsg  6692  tfindsg2  6693  nnsuc  6714  findsg  6725  suppssr  6951  tfrlem9  7108  oe0lem  7220  oa00  7265  omwordi  7277  om00  7281  omass  7286  oelim2  7301  oeoa  7303  oeoe  7305  nnmwordi  7341  swoso  7399  dom2lem  7614  onsdominel  7726  f1finf1o  7803  cantnfp1lem3  8190  cantnfp1  8191  cantnflem1  8199  rankr1ai  8274  rankval3b  8302  harcard  8417  infxpenlem  8449  alephnbtwn  8507  alephinit  8531  infxp  8650  cofsmo  8704  infpssALT  8748  fin23lem24  8757  fin56  8828  ttukeylem6  8949  ficard  8995  alephval2  9002  fpwwe2lem8  9067  fpwwe2  9073  gchcda1  9086  pwfseqlem3  9090  pwfseqlem4a  9091  pwfseqlem4  9092  gchpwdom  9100  tskss  9188  inar1  9205  gruss  9226  gruurn  9228  ltsonq  9399  distrlem4pr  9456  sqgt0sr  9535  map2psrpr  9539  letric  9739  renegcli  9940  addid0  10046  mulge0b  10482  nnge1  10642  0mnnnnn0  10909  nn0lt2  11007  zneo  11025  uzind2  11035  fzind  11040  nn0ind-raph  11042  uzwo  11229  nn01to3  11264  zbtwnre  11269  rpnnen1lem5  11301  xrletri  11457  qsqueeze  11501  difreicc  11771  elfzmlbp  11909  difelfznle  11912  elfzodifsumelfzo  11987  ssfzo12  12011  elfzonelfzo  12018  flflp1  12050  fleqceilz  12088  om2uzf1oi  12174  facdiv  12479  facwordi  12481  bcpasc  12513  hashdom  12565  hashle00  12584  ccatsymb  12734  swrdsbslen  12811  swrdspsleq  12812  swrdlsw  12815  swrdswrdlem  12822  swrdccatin1  12846  swrdccatin12lem3  12853  repswswrd  12894  cshwidx0  12914  cshwcsh2id  12934  limsupbnd1  13556  limsupbnd1OLD  13557  lo1bdd2  13600  addcn2  13669  mulcn2  13671  o1rlimmul  13694  lo1add  13702  lo1mul  13703  rlimno1  13729  znnenlem  14276  ruclem3  14297  odd2np1  14377  bitsfzo  14421  prmn2uzge3  14656  pcdvdsb  14830  pcaddlem  14845  infpnlem1  14866  prmunb  14870  vdwlem9  14951  vdwnnlem3  14959  ramcl  14999  prmgaplem5  15037  cshwshash  15087  setcmon  15994  setcepi  15995  setciso  15998  ghmf1  16923  sylow2alem2  17282  sylow2blem3  17286  qusabl  17515  lt6abl  17541  cyggexb  17545  gsumcom2  17619  imasring  17859  f1rhm0to0  17980  drnginvrcl  18004  drnginvrl  18006  drnginvrr  18007  subrgdvds  18034  lsmelval2  18320  quscrng  18476  mplsubrglem  18675  gsummoncoe1  18910  xrsdsreclblem  19026  obs2ss  19304  obslbs  19305  mp2pm2mplem4  19845  chfacfisf  19890  chfacfisfcpmat  19891  cayleyhamilton1  19928  cmpsublem  20426  cmpsub  20427  1stccnp  20489  locfincf  20558  txhaus  20674  xkohaus  20680  ufilss  20932  cfinufil  20955  fmfnfmlem1  20981  hausflim  21008  fclscf  21052  alexsubb  21073  qustgplem  21147  prdsbl  21518  metss2lem  21538  nghmcn  21778  cfil3i  22251  cmetcaulem  22270  minveclem4  22386  minveclem4OLD  22398  ovolgelb  22445  ovolunnul  22465  ovoliun  22470  ovoliunnul  22472  ovolicc2lem2  22483  iundisj2  22514  voliunlem3  22517  rolle  22954  dvlip  22957  lhop1lem  22977  lhop2  22979  dvfsumrlim  22995  deg1ge  23059  coeeulem  23190  dgrco  23241  radcnvlt1  23385  psercnlem1  23392  logcnlem2  23600  logcnlem3  23601  cxpeq  23709  angpined  23768  efrlim  23907  dmgmaddn0  23960  lgamucov  23975  basellem2  24020  ppieq0  24115  mumullem2  24119  chpeq0  24148  chteq0  24149  chtub  24152  fsumvma  24153  dchrptlem1  24204  bposlem6  24229  lgseisenlem2  24290  2sqlem6  24309  dchrisum0lem1  24366  pntrsumbnd2  24417  pntlem3  24459  colinearalg  24952  eengtrkg  25027  wlkv0  25500  0clwlk  25505  clwwlkgt0  25511  clwlkisclwwlklem2a4  25524  clwlkisclwwlklem1  25527  nbhashuvtx1  25655  dvrunz  26173  blocni  26458  ubthlem1  26524  minvecolem4  26534  minvecolem4OLD  26544  shmodsi  27054  atcvati  28051  atcvat2i  28052  chirredlem4  28058  atmd2  28065  sumdmdlem  28083  addltmulALT  28111  iundisj2f  28212  iundisj2fi  28385  rngurd  28563  erdszelem9  29934  rdgprc  30453  soseq  30504  cgrsub  30824  btwnxfr  30835  lineext  30855  linecgr  30860  btwnconn1lem4  30869  btwnconn1lem5  30870  btwnconn1lem6  30871  btwnconn1lem8  30873  btwnconn1lem11  30876  mptsnunlem  31752  finxpreclem6  31800  ltflcei  31945  poimirlem23  31975  poimirlem24  31976  poimirlem31  31983  poimirlem32  31984  ftc1anclem5  32033  heiborlem6  32160  grpokerinj  32195  isdmn3  32319  dmncan1  32321  l1cvpat  32632  atnle  32895  cvlexch3  32910  cvlexch4N  32911  cvlatexchb1  32912  cvrat2  33006  atlelt  33015  3dimlem4a  33040  3dimlem4OLDN  33042  ps-1  33054  ps-2  33055  4atlem10  33183  4atlem11  33186  4atlem12  33189  cdleme11c  33839  cdleme21c  33906  cdlemg6d  34200  trlcoat  34302  tendoid0  34404  cdleml3N  34557  dia2dimlem7  34650  pellexlem1  35685  pellexlem6  35690  imasgim  35970  iunrelexpmin1  36312  iunrelexpmin2  36316  radcnvrat  36674  nzss  36677  elprneb  38722  stgoldbwt  38887  sgoldbaltlem1  38890  pfxccat3a  38980  riotaeqimp  39047  zm1nn  39059  lesubnn0  39060  2ffzoeq  39074  incistruhgr  39181  is01wlklem  39721  usgra2pthspth  39769  lmod0rng  39972  0ring1eq0  39976  lidldomn1  40025  rngciso  40088  rngcisoALTV  40100  ringciso  40139  ringcisoALTV  40163  ztprmneprm  40232  lincresunit3  40378  aacllem  40644
  Copyright terms: Public domain W3C validator