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

Theorem syl2anb 476
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 469 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2b 472 1  |-  ( (
ph  /\  ta )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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  df-an 371
This theorem is referenced by:  sylancb  660  2eu6  2371  reupick3  3632  difprsnss  4006  pwssun  4623  trin2  5218  fnun  5514  fco  5565  f1co  5612  foco  5627  f1oun  5657  f1oco  5660  eqfnfv  5794  eqfunfv  5799  sorpsscmpl  6370  ordsucsssuc  6433  ordsucun  6435  soxp  6684  ressuppssdif  6709  issmo  6805  tfrlem5  6835  ener  7352  domtr  7358  unen  7388  xpdom2  7402  mapen  7471  unxpdomlem3  7515  fiin  7668  suc11reg  7821  xpnum  8117  pm54.43  8166  r0weon  8175  fseqen  8193  kmlem9  8323  axpre-lttrn  9329  axpre-mulgt0  9331  wloglei  9868  mulnzcnopr  9978  zaddcl  10681  zmulcl  10689  qaddcl  10965  qmulcl  10967  rpaddcl  11007  rpmulcl  11008  rpdivcl  11009  xrltnsym  11110  xrlttri  11112  xmullem  11223  xmulcom  11225  xmulneg1  11228  xmulf  11231  ge0addcl  11393  ge0mulcl  11394  ge0xaddcl  11395  ge0xmulcl  11396  serge0  11856  expclzlem  11885  expge0  11896  expge1  11897  hashfacen  12203  xpnnenOLD  13488  qredeu  13789  nn0gcdsq  13826  mul4sq  14011  fpwipodrs  15330  gimco  15789  gictr  15796  symgextf1  15919  efgrelexlemb  16240  xrs1mnd  17810  lmimco  18232  lmictra  18233  iscn2  18801  iscnp2  18802  paste  18857  txuni  19124  txcn  19158  txcmpb  19176  tx2ndc  19183  hmphtr  19315  snfil  19396  supfil  19427  filssufilg  19443  tsmsxp  19688  dscmet  20124  rlimcnp  22318  efnnfsumcl  22399  efchtdvds  22456  lgsne0  22631  mul2sq  22663  colinearalglem2  23088  nb3graprlem2  23295  wlkntrllem3  23395  ablosn  23769  ablomul  23777  hsn0elch  24586  shscli  24655  hsupss  24679  5oalem6  24997  mdsldmd1i  25670  superpos  25693  ghomsn  27236  sspred  27562  poseq  27643  wfrlem4  27656  frrlem4  27700  sltsolem1  27738  fnsingle  27879  funimage  27888  funpartfun  27903  riscer  28719  divrngidl  28753  mzpincl  28995  kelac2lem  29342  tz6.12-1-afv  30005  wwlktovf1  30177  wlknwwlknsur  30269  wlkiswwlksur  30276  wwlkextinj  30287  frgra3v  30519  scmatsubcl  30767  scmatmulcl  30769  bnj110  31685  bj-snsetex  32186
  Copyright terms: Public domain W3C validator