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

Theorem sylibrd 234
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 223 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 44 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:  3imtr4d  268  sbciegft  3362  eqsbc3r  3393  ordtr2  4922  elreldm  5227  ssimaex  5932  fconstfv  6123  fliftfun  6198  isopolem  6229  isosolem  6231  ordsucss  6637  f1oweALT  6768  fnse  6900  brtpos  6964  issmo2  7020  seqomlem1  7115  omcl  7186  oecl  7187  oawordeulem  7203  oaass  7210  omordi  7215  omord  7217  odi  7228  oen0  7235  oeordi  7236  oeordsuc  7243  nnmcl  7261  nnecl  7262  nnmordi  7280  nnmord  7281  nnmwordri  7285  nnaordex  7287  swoord1  7340  ecopovtrn  7414  f1domg  7535  pw2f1olem  7621  domtriord  7663  mapen  7681  mapxpen  7683  mapunen  7686  nndomo  7711  inficl  7885  supmo  7912  inf3lem6  8050  cantnflem1  8108  cantnflem1OLD  8131  tcmin  8172  tcrank  8302  cardne  8346  cardlim  8353  cardsdomel  8355  carduni  8362  alephord  8456  cardinfima  8478  dfac5lem4  8507  infdif2  8590  cofsmo  8649  cfcoflem  8652  infpssrlem4  8686  infpssrlem5  8687  fin4en1  8689  isfin2-2  8699  enfin2i  8701  fin23lem27  8708  isf32lem12  8744  isf34lem6  8760  domtriomlem  8822  cardmin  8939  fpwwe2lem12  9019  inar1  9153  gruiun  9177  ltsonq  9347  prub  9372  reclem3pr  9427  mulcmpblnr  9448  mulgt0sr  9482  axpre-sup  9546  leltadd  10036  infm3  10502  peano5nni  10539  zextle  10934  prime  10941  uzindOLD  10955  uzin  11114  ublbneg  11166  zbtwnre  11180  xrre2  11371  xralrple  11404  xmulneg1  11461  supxrbnd  11520  supxrgtmnf  11521  fzrevral  11762  flge  11910  ceile  11944  modadd1  12001  modmul1  12008  seqcl2  12093  facdiv  12333  hashss  12439  hash2prb  12483  elfzelfzccat  12563  repswswrd  12719  cshwcsh2id  12759  rlim2lt  13283  rlim3  13284  o1lo1  13323  climshftlem  13360  o1co  13372  o1of2  13398  isercolllem2  13451  isercoll  13453  caucvgrlem2  13460  climcndslem2  13625  sqrt2irr  13843  dvds2lem  13857  dvdsle  13890  dvdsfac  13900  divalglem0  13910  ndvdsadd  13925  bitsinv1lem  13950  sadcaddlem  13966  dvdslegcd  14013  bezoutlem2  14036  bezoutlem4  14038  gcdeq  14049  algcvga  14067  prmind2  14087  isprm6  14109  rpexp  14120  rpdvds  14124  eulerthlem2  14171  pclem  14221  pceulem  14228  pc2dvds  14261  fldivp1  14275  infpnlem1  14287  prmunb  14291  mrieqv2d  14894  plttr  15457  clatl  15603  issubg4  16025  gexdvds  16410  pgpssslw  16440  sylow2alem2  16444  efgs1b  16560  efgsfo  16563  lspindpi  17578  pf1ind  18190  psgnodpm  18419  psgndif  18433  obselocv  18554  mdetunilem9  18917  fiinbas  19248  bastg  19262  tgcl  19265  opnssneib  19410  clslp  19443  tgcnp  19548  iscnp4  19558  cncls2  19568  cncls  19569  cnntr  19570  cnpresti  19583  lmss  19593  lmcnp  19599  cmpsub  19694  tgcmp  19695  dfcon2  19714  t1conperf  19731  1stcfb  19740  1stcrest  19748  kgenss  19807  llycmpkgen2  19814  txdis  19896  qtoptop2  19963  kqt0lem  20000  isr0  20001  regr1lem2  20004  cmphaushmeo  20064  fbun  20104  ssfg  20136  fgtr  20154  ufildr  20195  cnpflf  20265  fclsnei  20283  flimfnfcls  20292  fclscmp  20294  ufilcmp  20296  cnpfcf  20305  alexsublem  20307  alexsubALTlem3  20312  alexsubALTlem4  20313  ptcmplem3  20317  tgphaus  20378  tgpt1  20379  tsmsresOLD  20408  tsmsres  20409  imasdsf1olem  20639  xblss2ps  20667  xblss2  20668  blsscls2  20770  metequiv2  20776  stdbdxmet  20781  nmoi  20998  reconn  21096  mulc1cncf  21172  cncfco  21174  iccpnfhmeo  21208  xrhmeo  21209  evth  21222  pi1grplem  21312  fgcfil  21473  ivthlem2  21627  ivthlem3  21628  ovolicc2lem4  21694  voliunlem1  21723  ioombl1lem4  21734  itg2gt0  21930  limcco  22060  lhop1  22178  tdeglem4  22221  plypf1  22372  coeeulem  22384  coeidlem  22397  coeid3  22400  plymul0or  22439  dvnply2  22445  plydivex  22455  vieta1lem2  22469  plyexmo  22471  aaliou3lem2  22501  ulmss  22554  ulmdvlem3  22559  iblulm  22564  sincosq2sgn  22653  sincosq3sgn  22654  sincosq4sgn  22655  logcnlem5  22783  dcubic  22933  amgm  23076  isnsqf  23165  mumullem2  23210  chtublem  23242  chtub  23243  fsumvma2  23245  vmasum  23247  dchrfi  23286  bposlem1  23315  bposlem3  23317  bposlem7  23321  lgsdir  23361  lgsquadlem2  23386  2sqlem8a  23402  2sqlem10  23405  dchrisum0flb  23451  pntpbnd1  23527  pntlemf  23546  pntlem3  23550  axeuclid  23970  umisuhgra  24031  uslisushgra  24067  uslisumgra  24068  usisuslgra  24069  constr3trl  24363  constr3pth  24364  wwlknext  24428  wwlkextsur  24435  clwwisshclwwlem1  24509  vdusgraval  24611  gxcl  24971  isexid2  25031  lnon0  25417  normpyc  25767  ocsh  25905  ocorth  25913  ococss  25915  shsel2  25944  hsupss  25963  pjhth  26015  shlub  26036  cm2j  26242  lnfncnbd  26680  riesz1  26688  rnbra  26730  leopadd  26755  leopmuli  26756  hstles  26854  stge1i  26861  stle0i  26862  dmdbr5  26931  ssmd2  26935  superpos  26977  chcv1  26978  atoml2i  27006  chirredlem2  27014  atcvat3i  27019  mdsymlem5  27030  mdsymlem6  27031  sumdmdii  27038  sumdmdlem2  27042  mul2lt0bi  27265  isarchiofld  27498  sqsscirc2  27555  cnre2csqlem  27556  xrge0iifiso  27581  sigaclci  27800  eulerpartlemb  27975  ballotlemimin  28112  ballotlem7  28142  cvmlift2lem12  28427  dfon2lem8  28827  soseq  28939  segconeq  29265  ifscgr  29299  brofs2  29332  brifs2  29333  endofsegid  29340  tan2h  29652  fzmul  29864  fdc  29869  incsequz2  29873  sstotbnd2  29901  sstotbnd3  29903  totbndbnd  29916  ispridl2  30066  mpt2bi123f  30203  irrapxlem2  30391  pell14qrdich  30437  monotoddzz  30511  pw2f1ocnv  30611  iocinico  30812  stoweidlem62  31390  elfzelfzlble  31832  sbcim2g  32407  riotasvd  33777  lsator0sp  33816  lssatle  33830  lshpset2N  33934  lkrlspeqN  33986  omllaw2N  34059  cmtbr3N  34069  lecmtN  34071  cvlcvr1  34154  cvrval4N  34228  cvrat3  34256  3noncolr2  34263  4noncolr3  34267  3dimlem3  34275  3dimlem3OLDN  34276  3dimlem4  34278  3dimlem4OLDN  34279  llncvrlpln  34372  lplncvrlvol  34430  snatpsubN  34564  linepsubN  34566  pmapjat1  34667  pclfinclN  34764  pl42N  34797  ltrneq2  34962  cdleme7aa  35056  cdleme18d  35109  cdleme21b  35140  trlord  35383  trlcoat  35537  dochkrshp  36201  lcfl8  36317
  Copyright terms: Public domain W3C validator