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

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

Proof of Theorem sylibrd
StepHypRef Expression
1 sylibrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylibrd.2 . . 3  |-  ( ph  ->  ( th  <->  ch )
)
32biimprd 216 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 43 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  3imtr4d  261  sbciegft  3193  eqsbc3r  3220  ordtr2  4628  ordsucss  4801  elreldm  5097  ssimaex  5791  fconstfv  5957  fliftfun  6037  isopolem  6068  isosolem  6070  f1oweALT  6077  fnse  6466  brtpos  6491  riotasvd  6595  issmo2  6614  seqomlem1  6710  omcl  6783  oecl  6784  oawordeulem  6800  oaass  6807  omordi  6812  omord  6814  odi  6825  oen0  6832  oeordi  6833  oeordsuc  6840  nnmcl  6858  nnecl  6859  nnmordi  6877  nnmord  6878  nnmwordri  6882  nnaordex  6884  swoord1  6937  ecopovtrn  7010  f1domg  7130  pw2f1olem  7215  domtriord  7256  mapen  7274  mapxpen  7276  mapunen  7279  nndomo  7303  inficl  7433  supmo  7460  inf3lem6  7591  cantnflem1  7648  tcmin  7683  tcrank  7813  cardne  7857  cardlim  7864  cardsdomel  7866  carduni  7873  alephord  7961  cardinfima  7983  dfac5lem4  8012  infdif2  8095  cofsmo  8154  cfcoflem  8157  infpssrlem4  8191  infpssrlem5  8192  fin4en1  8194  isfin2-2  8204  enfin2i  8206  fin23lem27  8213  isf32lem12  8249  isf34lem6  8265  domtriomlem  8327  cardmin  8444  fpwwe2lem12  8521  inar1  8655  gruiun  8679  ltsonq  8851  prub  8876  reclem3pr  8931  mulcmpblnr  8954  mulgt0sr  8985  axpre-sup  9049  leltadd  9517  infm3  9972  peano5nni  10008  zextle  10348  prime  10355  uzindOLD  10369  uzin  10523  ublbneg  10565  zbtwnre  10577  xrre2  10763  xralrple  10796  xmulneg1  10853  supxrbnd  10912  supxrgtmnf  10913  fzrevral  11136  flge  11219  ceile  11240  modadd1  11283  modmul1  11284  seqcl2  11346  facdiv  11583  hash2prb  11694  rlim2lt  12296  rlim3  12297  o1lo1  12336  climshftlem  12373  o1co  12385  o1of2  12411  isercolllem2  12464  isercoll  12466  caucvgrlem2  12473  climcndslem2  12635  sqr2irr  12853  dvds2lem  12867  dvdsle  12900  dvdsfac  12909  divalglem0  12918  ndvdsadd  12933  bitsinv1lem  12958  sadcaddlem  12974  dvdslegcd  13021  bezoutlem2  13044  bezoutlem4  13046  gcdeq  13057  algcvga  13075  prmind2  13095  isprm6  13114  rpexp  13125  rpdvds  13129  eulerthlem2  13176  pclem  13217  pceulem  13224  pc2dvds  13257  fldivp1  13271  infpnlem1  13283  prmunb  13287  mrieqv2d  13869  plttr  14432  joinlem  14452  meetlem  14459  issubg4  14966  gexdvds  15223  pgpssslw  15253  sylow2alem2  15257  efgs1b  15373  efgsfo  15376  lspindpi  16209  obselocv  16960  fiinbas  17022  bastg  17036  tgcl  17039  opnssneib  17184  clslp  17217  tgcnp  17322  iscnp4  17332  cncls2  17342  cncls  17343  cnntr  17344  cnpresti  17357  lmss  17367  lmcnp  17373  cmpsub  17468  tgcmp  17469  dfcon2  17487  t1conperf  17504  1stcfb  17513  1stcrest  17521  kgenss  17580  llycmpkgen2  17587  txdis  17669  qtoptop2  17736  kqt0lem  17773  isr0  17774  regr1lem2  17777  cmphaushmeo  17837  fbun  17877  ssfg  17909  fgtr  17927  ufildr  17968  cnpflf  18038  fclsnei  18056  flimfnfcls  18065  fclscmp  18067  ufilcmp  18069  cnpfcf  18078  alexsublem  18080  alexsubALTlem3  18085  alexsubALTlem4  18086  ptcmplem3  18090  tgphaus  18151  tgpt1  18152  tsmsres  18178  imasdsf1olem  18408  xblss2ps  18436  xblss2  18437  blsscls2  18539  metequiv2  18545  stdbdxmet  18550  nmoi  18767  reconn  18864  mulc1cncf  18940  cncfco  18942  iccpnfhmeo  18975  xrhmeo  18976  evth  18989  pi1grplem  19079  fgcfil  19229  ivthlem2  19354  ivthlem3  19355  ovolicc2lem4  19421  voliunlem1  19449  ioombl1lem4  19460  itg2gt0  19655  limcco  19785  lhop1  19903  pf1ind  19980  tdeglem4  19988  plypf1  20136  coeeulem  20148  coeidlem  20161  coeid3  20164  plymul0or  20203  dvnply2  20209  plydivex  20219  vieta1lem2  20233  plyexmo  20235  aaliou3lem2  20265  ulmss  20318  ulmdvlem3  20323  iblulm  20328  sincosq2sgn  20412  sincosq3sgn  20413  sincosq4sgn  20414  logcnlem5  20542  dcubic  20691  amgm  20834  isnsqf  20923  mumullem2  20968  chtublem  21000  chtub  21001  fsumvma2  21003  vmasum  21005  dchrfi  21044  bposlem1  21073  bposlem3  21075  bposlem7  21079  lgsdir  21119  lgsquadlem2  21144  2sqlem8a  21160  2sqlem10  21163  dchrisum0flb  21209  pntpbnd1  21285  pntlemf  21304  pntlem3  21308  umisuhgra  21367  uslisumgra  21391  usisuslgra  21392  constr3trl  21651  constr3pth  21652  vdusgraval  21683  gxcl  21858  isexid2  21918  lnon0  22304  normpyc  22653  ocsh  22790  ocorth  22798  ococss  22800  shsel2  22829  hsupss  22848  pjhth  22900  shlub  22921  cm2j  23127  lnfncnbd  23565  riesz1  23573  rnbra  23615  leopadd  23640  leopmuli  23641  hstles  23739  stge1i  23746  stle0i  23747  dmdbr5  23816  ssmd2  23820  superpos  23862  chcv1  23863  atoml2i  23891  chirredlem2  23899  atcvat3i  23904  mdsymlem5  23915  mdsymlem6  23916  sumdmdii  23923  sumdmdlem2  23927  sqsscirc2  24312  cnre2csqlem  24313  xrge0iifiso  24326  sigaclci  24520  ballotlemimin  24768  ballotlem7  24798  cvmlift2lem12  25006  dfon2lem8  25422  soseq  25534  axeuclid  25907  segconeq  25949  ifscgr  25983  brofs2  26016  brifs2  26017  endofsegid  26024  tan2h  26252  fzmul  26457  fdc  26462  incsequz2  26466  sstotbnd2  26496  sstotbnd3  26498  totbndbnd  26511  ispridl2  26661  irrapxlem2  26899  pell14qrdich  26945  monotoddzz  27019  pw2f1ocnv  27121  stoweidlem62  27800  hashss  28191  elfzelfzccat  28208  2cshw2lem1  28285  sbcim2g  28696  lsator0sp  29872  lssatle  29886  lshpset2N  29990  lkrlspeqN  30042  omllaw2N  30115  cmtbr3N  30125  lecmtN  30127  cvlcvr1  30210  cvrval4N  30284  cvrat3  30312  3noncolr2  30319  4noncolr3  30323  3dimlem3  30331  3dimlem3OLDN  30332  3dimlem4  30334  3dimlem4OLDN  30335  llncvrlpln  30428  lplncvrlvol  30486  snatpsubN  30620  linepsubN  30622  pmapjat1  30723  pclfinclN  30820  pl42N  30853  ltrneq2  31018  cdleme7aa  31112  cdleme18d  31165  cdleme21b  31196  trlord  31439  trlcoat  31593  dochkrshp  32257  lcfl8  32373
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 179
  Copyright terms: Public domain W3C validator