MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylbird Structured 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 46 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  3203  eqreu  3264  sotr2  4801  sossfld  5300  ordtr3  5485  ordintdif  5489  tz6.12i  5899  soisoi  6232  ov3  6445  tfindsg  6699  tfindsg2  6700  nnsuc  6721  findsg  6732  suppssr  6955  tfrlem9  7109  oe0lem  7221  oa00  7266  omwordi  7278  om00  7282  omass  7287  oelim2  7302  oeoa  7304  oeoe  7306  nnmwordi  7342  swoso  7400  dom2lem  7614  onsdominel  7725  f1finf1o  7802  cantnfp1lem3  8188  cantnfp1  8189  cantnflem1  8197  rankr1ai  8272  rankval3b  8300  harcard  8415  infxpenlem  8447  alephnbtwn  8504  alephinit  8528  infxp  8647  cofsmo  8701  infpssALT  8745  fin23lem24  8754  fin56  8825  ttukeylem6  8946  ficard  8992  alephval2  8999  fpwwe2lem8  9064  fpwwe2  9070  gchcda1  9083  pwfseqlem3  9087  pwfseqlem4a  9088  pwfseqlem4  9089  gchpwdom  9097  tskss  9185  inar1  9202  gruss  9223  gruurn  9225  ltsonq  9396  distrlem4pr  9453  sqgt0sr  9532  map2psrpr  9536  letric  9736  renegcli  9937  mulge0b  10477  nnge1  10637  0mnnnnn0  10904  nn0lt2  11002  zneo  11020  uzind2  11030  fzind  11035  nn0ind-raph  11037  uzwo  11224  nn01to3  11259  zbtwnre  11264  rpnnen1lem5  11296  xrletri  11452  qsqueeze  11496  difreicc  11766  elfzmlbp  11904  difelfznle  11907  elfzodifsumelfzo  11981  ssfzo12  12005  elfzonelfzo  12012  flflp1  12044  fleqceilz  12082  om2uzf1oi  12168  facdiv  12473  facwordi  12475  bcpasc  12507  hashdom  12559  hashle00  12578  ccatsymb  12725  swrdsbslen  12800  swrdspsleq  12801  swrdlsw  12804  swrdswrdlem  12811  swrdccatin1  12835  swrdccatin12lem3  12842  repswswrd  12883  cshwidx0  12903  cshwcsh2id  12923  limsupbnd1  13537  limsupbnd1OLD  13538  lo1bdd2  13581  addcn2  13650  mulcn2  13652  o1rlimmul  13675  lo1add  13683  lo1mul  13684  rlimno1  13710  znnenlem  14257  ruclem3  14278  odd2np1  14358  bitsfzo  14402  prmn2uzge3  14637  pcdvdsb  14811  pcaddlem  14826  infpnlem1  14847  prmunb  14851  vdwlem9  14932  vdwnnlem3  14940  ramcl  14980  prmgaplem5  15018  cshwshash  15068  setcmon  15975  setcepi  15976  setciso  15979  ghmf1  16904  sylow2alem2  17263  sylow2blem3  17267  qusabl  17496  lt6abl  17522  cyggexb  17526  gsumcom2  17600  imasring  17840  f1rhm0to0  17961  drnginvrcl  17985  drnginvrl  17987  drnginvrr  17988  subrgdvds  18015  lsmelval2  18301  quscrng  18457  mplsubrglem  18656  gsummoncoe1  18891  xrsdsreclblem  19007  obs2ss  19284  obslbs  19285  mp2pm2mplem4  19825  chfacfisf  19870  chfacfisfcpmat  19871  cayleyhamilton1  19908  cmpsublem  20406  cmpsub  20407  1stccnp  20469  locfincf  20538  txhaus  20654  xkohaus  20660  ufilss  20912  cfinufil  20935  fmfnfmlem1  20961  hausflim  20988  fclscf  21032  alexsubb  21053  qustgplem  21127  prdsbl  21498  metss2lem  21518  nghmcn  21758  cfil3i  22231  cmetcaulem  22250  minveclem4  22366  minveclem4OLD  22378  ovolgelb  22425  ovolunnul  22445  ovoliun  22450  ovoliunnul  22452  ovolicc2lem2  22463  iundisj2  22494  voliunlem3  22497  rolle  22934  dvlip  22937  lhop1lem  22957  lhop2  22959  dvfsumrlim  22975  deg1ge  23039  coeeulem  23170  dgrco  23221  radcnvlt1  23365  psercnlem1  23372  logcnlem2  23580  logcnlem3  23581  cxpeq  23689  angpined  23748  efrlim  23887  dmgmaddn0  23940  lgamucov  23955  basellem2  24000  ppieq0  24095  mumullem2  24099  chpeq0  24128  chteq0  24129  chtub  24132  fsumvma  24133  dchrptlem1  24184  bposlem6  24209  lgseisenlem2  24270  2sqlem6  24289  dchrisum0lem1  24346  pntrsumbnd2  24397  pntlem3  24439  colinearalg  24932  eengtrkg  25007  wlkv0  25480  0clwlk  25485  clwwlkgt0  25491  clwlkisclwwlklem2a4  25504  clwlkisclwwlklem1  25507  nbhashuvtx1  25635  dvrunz  26153  blocni  26438  ubthlem1  26504  minvecolem4  26514  minvecolem4OLD  26524  shmodsi  27034  atcvati  28031  atcvat2i  28032  chirredlem4  28038  atmd2  28045  sumdmdlem  28063  addltmulALT  28091  iundisj2f  28196  iundisj2fi  28373  rngurd  28553  erdszelem9  29924  rdgprc  30442  soseq  30493  cgrsub  30811  btwnxfr  30822  lineext  30842  linecgr  30847  btwnconn1lem4  30856  btwnconn1lem5  30857  btwnconn1lem6  30858  btwnconn1lem8  30860  btwnconn1lem11  30863  mptsnunlem  31698  finxpreclem6  31746  ltflcei  31891  poimirlem23  31921  poimirlem24  31922  poimirlem31  31929  poimirlem32  31930  ftc1anclem5  31979  heiborlem6  32106  grpokerinj  32141  isdmn3  32265  dmncan1  32267  l1cvpat  32583  atnle  32846  cvlexch3  32861  cvlexch4N  32862  cvlatexchb1  32863  cvrat2  32957  atlelt  32966  3dimlem4a  32991  3dimlem4OLDN  32993  ps-1  33005  ps-2  33006  4atlem10  33134  4atlem11  33137  4atlem12  33140  cdleme11c  33790  cdleme21c  33857  cdlemg6d  34151  trlcoat  34253  tendoid0  34355  cdleml3N  34508  dia2dimlem7  34601  pellexlem1  35637  pellexlem6  35642  imasgim  35922  iunrelexpmin1  36204  iunrelexpmin2  36208  radcnvrat  36565  nzss  36568  elprneb  38468  stgoldbwt  38633  sgoldbaltlem1  38636  pfxccat3a  38726  zm1nn  38782  lesubnn0  38783  2ffzoeq  38797  usgra2pthspth  39007  lmod0rng  39210  0ring1eq0  39214  lidldomn1  39263  rngciso  39326  rngcisoALTV  39338  ringciso  39377  ringcisoALTV  39401  ztprmneprm  39472  lincresunit3  39618  aacllem  39884
  Copyright terms: Public domain W3C validator