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

Theorem syl2anb 466
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 459 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2b 462 1  |-  ( (
ph  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  sylancb  647  2eu6  2343  reupick3  3590  difprsnss  3898  pwssun  4453  ordsucsssuc  4766  ordsucun  4768  trin2  5220  fnun  5514  fco  5563  f1co  5611  foco  5626  f1oun  5657  f1oco  5661  eqfnfv  5790  eqfunfv  5795  soxp  6422  sorpsscmpl  6496  issmo  6573  ener  7117  domtr  7123  unen  7152  xpdom2  7166  mapen  7234  unxpdomlem3  7278  fiin  7389  suc11reg  7534  xpnum  7798  pm54.43  7847  r0weon  7854  fseqen  7868  kmlem9  7998  axpre-lttrn  9001  axpre-mulgt0  9003  wloglei  9519  mulnzcnopr  9628  zaddcl  10277  zmulcl  10284  qaddcl  10550  qmulcl  10552  rpaddcl  10592  rpmulcl  10593  rpdivcl  10594  xrltnsym  10690  xrlttri  10692  xmullem  10803  xmulcom  10805  xmulneg1  10808  xmulf  10811  ge0addcl  10969  ge0mulcl  10970  ge0xaddcl  10971  ge0xmulcl  10972  serge0  11336  expclzlem  11364  expge0  11375  expge1  11376  hashfacen  11662  xpnnenOLD  12768  qredeu  13066  nn0gcdsq  13103  mul4sq  13281  fpwipodrs  14549  gimco  15014  gictr  15021  efgrelexlemb  15341  xrs1mnd  16695  iscn2  17260  iscnp2  17261  paste  17316  txuni  17581  txcn  17615  txcmpb  17633  tx2ndc  17640  hmphtr  17772  snfil  17853  supfil  17884  filssufilg  17900  tsmsxp  18141  dscmet  18577  rlimcnp  20761  efnnfsumcl  20842  efchtdvds  20899  lgsne0  21074  mul2sq  21106  nb3graprlem2  21418  wlkntrllem3  21518  ablosn  21892  ablomul  21900  hsn0elch  22707  shscli  22776  hsupss  22800  5oalem6  23118  mdsldmd1i  23791  superpos  23814  ghomsn  25056  sspred  25392  poseq  25471  wfrlem4  25477  frrlem4  25502  sltsolem1  25540  fnsingle  25676  funimage  25685  funpartfun  25700  colinearalglem2  25754  riscer  26498  divrngidl  26532  mzpincl  26685  kelac2lem  27034  tz6.12-1-afv  27909  swrd0swrd  28013  frgra3v  28110  bnj110  28939
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 178  df-an 361
  Copyright terms: Public domain W3C validator