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

Theorem sylbird 235
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 223 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbird.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 42 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3imtr3d  267  ceqex  3179  eqreu  3240  sotr2  4772  sossfld  5270  ordtr3  5454  ordintdif  5458  tz6.12i  5868  suppssrOLD  5998  soisoi  6206  ov3  6419  tfindsg  6677  tfindsg2  6678  nnsuc  6699  findsg  6710  suppssr  6933  tfrlem9  7087  oe0lem  7199  oa00  7244  omwordi  7256  om00  7260  omass  7265  oelim2  7280  oeoa  7282  oeoe  7284  nnmwordi  7320  swoso  7378  dom2lem  7592  onsdominel  7703  f1finf1o  7780  cantnfp1lem3  8130  cantnfp1  8131  cantnflem1  8139  cantnfp1lem3OLD  8156  cantnfp1OLD  8157  cantnflem1OLD  8162  rankr1ai  8247  rankval3b  8275  harcard  8390  infxpenlem  8422  alephnbtwn  8483  alephinit  8507  infxp  8626  cofsmo  8680  infpssALT  8724  fin23lem24  8733  fin56  8804  ttukeylem6  8925  ficard  8971  alephval2  8978  fpwwe2lem8  9044  fpwwe2  9050  gchcda1  9063  pwfseqlem3  9067  pwfseqlem4a  9068  pwfseqlem4  9069  gchpwdom  9077  tskss  9165  inar1  9182  gruss  9203  gruurn  9205  ltsonq  9376  distrlem4pr  9433  sqgt0sr  9512  map2psrpr  9516  letric  9715  renegcli  9915  mulge0b  10452  nnge1  10601  0mnnnnn0  10868  nn0lt2  10967  zneo  10985  uzind2  10995  fzind  11000  nn0ind-raph  11002  uzwo  11189  nn01to3  11219  zbtwnre  11224  rpnnen1lem5  11256  xrletri  11409  qsqueeze  11452  difreicc  11704  elfzmlbp  11839  difelfznle  11842  elfzodifsumelfzo  11916  ssfzo12  11940  elfzonelfzo  11947  flflp1  11979  fleqceilz  12017  om2uzf1oi  12103  facdiv  12407  facwordi  12409  bcpasc  12441  hashdom  12493  hashle00  12512  ccatsymb  12652  swrdsbslen  12727  swrdspsleq  12728  swrdlsw  12731  swrdswrdlem  12738  swrdccatin1  12762  swrdccatin12lem3  12769  repswswrd  12810  cshwidx0  12830  cshwcsh2id  12850  limsupbnd1  13452  lo1bdd2  13494  addcn2  13563  mulcn2  13565  o1rlimmul  13588  lo1add  13596  lo1mul  13597  rlimno1  13623  znnenlem  14152  ruclem3  14173  odd2np1  14253  bitsfzo  14292  prmn2uzge3  14444  pcdvdsb  14599  pcaddlem  14614  infpnlem1  14635  prmunb  14639  vdwlem9  14714  vdwnnlem3  14722  ramcl  14754  cshwshash  14796  setcmon  15688  setcepi  15689  setciso  15692  ghmf1  16617  sylow2alem2  16960  sylow2blem3  16964  qusabl  17193  lt6abl  17219  cyggexb  17223  gsumcom2  17322  imasring  17586  f1rhm0to0  17707  drnginvrcl  17731  drnginvrl  17733  drnginvrr  17734  subrgdvds  17761  lsmelval2  18049  quscrng  18206  mplsubrglem  18418  mplsubrglemOLD  18419  gsummoncoe1  18664  xrsdsreclblem  18782  obs2ss  19056  obslbs  19057  mp2pm2mplem4  19600  chfacfisf  19645  chfacfisfcpmat  19646  cayleyhamilton1  19683  cmpsublem  20190  cmpsub  20191  1stccnp  20253  locfincf  20322  txhaus  20438  xkohaus  20444  ufilss  20696  cfinufil  20719  fmfnfmlem1  20745  hausflim  20772  fclscf  20816  alexsubb  20836  qustgplem  20909  prdsbl  21284  metss2lem  21304  nghmcn  21542  cfil3i  21998  cmetcaulem  22017  minveclem4  22137  ovolgelb  22181  ovolunnul  22201  ovoliun  22206  ovoliunnul  22208  ovolicc2lem2  22219  iundisj2  22249  voliunlem3  22252  rolle  22681  dvlip  22684  lhop1lem  22704  lhop2  22706  dvfsumrlim  22722  deg1ge  22789  coeeulem  22911  dgrco  22962  radcnvlt1  23103  psercnlem1  23110  logcnlem2  23316  logcnlem3  23317  cxpeq  23425  angpined  23484  efrlim  23623  dmgmaddn0  23676  lgamucov  23691  basellem2  23734  ppieq0  23829  mumullem2  23833  chpeq0  23862  chteq0  23863  chtub  23866  fsumvma  23867  dchrptlem1  23918  bposlem6  23943  lgseisenlem2  24004  2sqlem6  24023  dchrisum0lem1  24080  pntrsumbnd2  24131  pntlem3  24173  colinearalg  24617  eengtrkg  24692  wlkv0  25164  0clwlk  25169  clwwlkgt0  25175  clwlkisclwwlklem2a4  25188  clwlkisclwwlklem1  25191  nbhashuvtx1  25319  dvrunz  25835  blocni  26120  ubthlem1  26186  minvecolem4  26196  shmodsi  26707  atcvati  27704  atcvat2i  27705  chirredlem4  27711  atmd2  27718  sumdmdlem  27736  addltmulALT  27764  iundisj2f  27868  iundisj2fi  28036  rngurd  28217  erdszelem9  29483  rdgprc  30001  soseq  30052  cgrsub  30370  btwnxfr  30381  lineext  30401  linecgr  30406  btwnconn1lem4  30415  btwnconn1lem5  30416  btwnconn1lem6  30417  btwnconn1lem8  30419  btwnconn1lem11  30422  mptsnunlem  31241  ltflcei  31395  ftc1anclem5  31447  heiborlem6  31574  grpokerinj  31609  isdmn3  31733  dmncan1  31735  l1cvpat  32052  atnle  32315  cvlexch3  32330  cvlexch4N  32331  cvlatexchb1  32332  cvrat2  32426  atlelt  32435  3dimlem4a  32460  3dimlem4OLDN  32462  ps-1  32474  ps-2  32475  4atlem10  32603  4atlem11  32606  4atlem12  32609  cdleme11c  33259  cdleme21c  33326  cdlemg6d  33620  trlcoat  33722  tendoid0  33824  cdleml3N  33977  dia2dimlem7  34070  pellexlem1  35106  pellexlem6  35111  imasgim  35392  iunrelexpmin1  35667  iunrelexpmin2  35671  radcnvrat  36023  nzss  36050  elprneb  37644  stgoldbwt  37811  sgoldbaltlem1  37814  pfxccat3a  37897  zm1nn  37938  lesubnn0  37939  2ffzoeq  37953  usgra2pthspth  37961  lmod0rng  38166  0ring1eq0  38170  lidldomn1  38219  rngciso  38282  rngcisoALTV  38294  ringciso  38333  ringcisoALTV  38357  ztprmneprm  38428  lincresunit3  38574  aacllem  38841
  Copyright terms: Public domain W3C validator