MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2anb Structured version   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  2366  reupick3  3626  difprsnss  3934  pwssun  4489  ordsucsssuc  4803  ordsucun  4805  trin2  5257  fnun  5551  fco  5600  f1co  5648  foco  5663  f1oun  5694  f1oco  5698  eqfnfv  5827  eqfunfv  5832  soxp  6459  sorpsscmpl  6533  issmo  6610  ener  7154  domtr  7160  unen  7189  xpdom2  7203  mapen  7271  unxpdomlem3  7315  fiin  7427  suc11reg  7574  xpnum  7838  pm54.43  7887  r0weon  7894  fseqen  7908  kmlem9  8038  axpre-lttrn  9041  axpre-mulgt0  9043  wloglei  9559  mulnzcnopr  9668  zaddcl  10317  zmulcl  10324  qaddcl  10590  qmulcl  10592  rpaddcl  10632  rpmulcl  10633  rpdivcl  10634  xrltnsym  10730  xrlttri  10732  xmullem  10843  xmulcom  10845  xmulneg1  10848  xmulf  10851  ge0addcl  11009  ge0mulcl  11010  ge0xaddcl  11011  ge0xmulcl  11012  serge0  11377  expclzlem  11405  expge0  11416  expge1  11417  hashfacen  11703  xpnnenOLD  12809  qredeu  13107  nn0gcdsq  13144  mul4sq  13322  fpwipodrs  14590  gimco  15055  gictr  15062  efgrelexlemb  15382  xrs1mnd  16736  iscn2  17302  iscnp2  17303  paste  17358  txuni  17624  txcn  17658  txcmpb  17676  tx2ndc  17683  hmphtr  17815  snfil  17896  supfil  17927  filssufilg  17943  tsmsxp  18184  dscmet  18620  rlimcnp  20804  efnnfsumcl  20885  efchtdvds  20942  lgsne0  21117  mul2sq  21149  nb3graprlem2  21461  wlkntrllem3  21561  ablosn  21935  ablomul  21943  hsn0elch  22750  shscli  22819  hsupss  22843  5oalem6  23161  mdsldmd1i  23834  superpos  23857  ghomsn  25099  sspred  25447  poseq  25528  wfrlem4  25541  frrlem4  25585  sltsolem1  25623  fnsingle  25764  funimage  25773  funpartfun  25788  colinearalglem2  25846  riscer  26604  divrngidl  26638  mzpincl  26791  kelac2lem  27139  tz6.12-1-afv  28014  swrd0swrd  28197  frgra3v  28392  bnj110  29229
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