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

Theorem syl2anb 465
Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
Hypotheses
Ref Expression
syl2anb.1  |-  ( ph  <->  ps )
syl2anb.2  |-  ( ta  <->  ch )
syl2anb.3  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
syl2anb  |-  ( (
ph  /\  ta )  ->  th )

Proof of Theorem syl2anb
StepHypRef Expression
1 syl2anb.2 . 2  |-  ( ta  <->  ch )
2 syl2anb.1 . . 3  |-  ( ph  <->  ps )
3 syl2anb.3 . . 3  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylanb 458 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2b 461 1  |-  ( (
ph  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  sylancb  646  2eu6  2228  reupick3  3453  difprsn  3756  pwssun  4299  ordsucsssuc  4614  ordsucun  4616  trin2  5066  fnun  5350  fco  5398  f1co  5446  foco  5461  f1oun  5492  f1oco  5496  eqfnfv  5622  eqfunfv  5627  soxp  6228  sorpsscmpl  6288  issmo  6365  ener  6908  domtr  6914  unen  6943  xpdom2  6957  mapen  7025  unxpdomlem3  7069  fiin  7175  suc11reg  7320  xpnum  7584  pm54.43  7633  r0weon  7640  fseqen  7654  kmlem9  7784  axpre-lttrn  8788  axpre-mulgt0  8790  wloglei  9305  mulnzcnopr  9414  zaddcl  10059  zmulcl  10066  qaddcl  10332  qmulcl  10334  rpaddcl  10374  rpmulcl  10375  rpdivcl  10376  xrltnsym  10471  xrlttri  10473  xmullem  10584  xmulcom  10586  xmulneg1  10589  xmulf  10592  ge0addcl  10748  ge0mulcl  10749  ge0xaddcl  10750  ge0xmulcl  10751  serge0  11100  expclzlem  11127  expge0  11138  expge1  11139  hashfacen  11392  xpnnenOLD  12488  qredeu  12786  nn0gcdsq  12823  mul4sq  13001  fpwipodrs  14267  gimco  14732  gictr  14739  efgrelexlemb  15059  xrs1mnd  16409  iscn2  16968  iscnp2  16969  paste  17022  txuni  17287  txcn  17320  txcmpb  17338  tx2ndc  17345  hmphtr  17474  snfil  17559  supfil  17590  filssufilg  17606  tsmsxp  17837  dscmet  18095  rlimcnp  20260  efnnfsumcl  20340  efchtdvds  20397  lgsne0  20572  mul2sq  20604  ablosn  21014  ablomul  21022  hsn0elch  21827  shscli  21896  hsupss  21920  5oalem6  22238  mdsldmd1i  22911  superpos  22934  dmgmseqn0  23696  ghomsn  23995  sspred  24174  poseq  24253  wfrlem4  24259  frrlem4  24284  sltsolem1  24322  fnsingle  24458  funimage  24467  funpartfun  24481  colinearalglem2  24535  trunitr  25109  cbcpcp  25162  inposet  25278  zintdom  25438  inttop2  25515  limptlimpr2lem2  25575  sigadd  25649  riscer  26619  divrngidl  26653  mzpincl  26812  kelac2lem  27162  frgra3v  28180  bnj110  28890
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator