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  2294  reupick3  3529  difprsnss  3832  pwssun  4381  ordsucsssuc  4696  ordsucun  4698  trin2  5148  fnun  5432  fco  5481  f1co  5529  foco  5544  f1oun  5575  f1oco  5579  eqfnfv  5705  eqfunfv  5710  soxp  6315  sorpsscmpl  6375  issmo  6452  ener  6996  domtr  7002  unen  7031  xpdom2  7045  mapen  7113  unxpdomlem3  7157  fiin  7265  suc11reg  7410  xpnum  7674  pm54.43  7723  r0weon  7730  fseqen  7744  kmlem9  7874  axpre-lttrn  8878  axpre-mulgt0  8880  wloglei  9395  mulnzcnopr  9504  zaddcl  10151  zmulcl  10158  qaddcl  10424  qmulcl  10426  rpaddcl  10466  rpmulcl  10467  rpdivcl  10468  xrltnsym  10563  xrlttri  10565  xmullem  10676  xmulcom  10678  xmulneg1  10681  xmulf  10684  ge0addcl  10840  ge0mulcl  10841  ge0xaddcl  10842  ge0xmulcl  10843  serge0  11192  expclzlem  11220  expge0  11231  expge1  11232  hashfacen  11488  xpnnenOLD  12585  qredeu  12883  nn0gcdsq  12920  mul4sq  13098  fpwipodrs  14366  gimco  14831  gictr  14838  efgrelexlemb  15158  xrs1mnd  16515  iscn2  17074  iscnp2  17075  paste  17128  txuni  17393  txcn  17426  txcmpb  17444  tx2ndc  17451  hmphtr  17580  snfil  17661  supfil  17692  filssufilg  17708  tsmsxp  17939  dscmet  18197  rlimcnp  20371  efnnfsumcl  20452  efchtdvds  20509  lgsne0  20684  mul2sq  20716  ablosn  21126  ablomul  21134  hsn0elch  21941  shscli  22010  hsupss  22034  5oalem6  22352  mdsldmd1i  23025  superpos  23048  ghomsn  24399  sspred  24732  poseq  24811  wfrlem4  24817  frrlem4  24842  sltsolem1  24880  fnsingle  25016  funimage  25025  funpartfun  25040  colinearalglem2  25094  riscer  25942  divrngidl  25976  mzpincl  26135  kelac2lem  26485  tz6.12-1-afv  27362  nb3graprlem2  27615  wlkntrllem5  27705  frgra3v  27835  bnj110  28652
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