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

Theorem syl2anb 599
Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
Hypotheses
Ref Expression
syl2anb.1 (𝜑𝜓)
syl2anb.2 (𝜏𝜒)
syl2anb.3 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
syl2anb ((𝜑𝜏) → 𝜃)

Proof of Theorem syl2anb
StepHypRef Expression
1 syl2anb.2 . 2 (𝜏𝜒)
2 syl2anb.1 . . 3 (𝜑𝜓)
3 syl2anb.3 . . 3 ((𝜓𝜒) → 𝜃)
42, 3sylanb 582 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2b 595 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  sylancb  601  rexdifi  4106  reupick3  4280  difprsnss  4760  opthhausdorff  5475  pwssun  5529  trin2  6078  sspred  6263  fundif  6551  fnun  6615  fcoOLD  6694  f1cof1  6750  f1coOLD  6752  f1oun  6804  f1oco  6808  eqfnfv  6983  eqfunfv  6988  sorpsscmpl  7672  ordsucsssuc  7759  ordsucun  7761  soxp  8062  poseq  8091  ressuppssdif  8117  frrlem4  8221  wfrlem4OLD  8259  issmo  8295  tfrlem5  8327  ener  8944  domtr  8950  unen  8993  xpdom2  9014  mapen  9088  unxpdomlem3  9199  fiin  9363  suc11reg  9560  djuunxp  9862  xpnum  9892  pm54.43  9942  r0weon  9953  fseqen  9968  kmlem9  10099  axpre-lttrn  11107  axpre-mulgt0  11109  wloglei  11692  mulnzcnopr  11806  zaddcl  12548  zmulcl  12557  qaddcl  12895  qmulcl  12897  rpaddcl  12942  rpmulcl  12943  rpdivcl  12945  xrltnsym  13062  xrlttri  13064  xmullem  13189  xmulcom  13191  xmulneg1  13194  xmulf  13197  ge0addcl  13383  ge0mulcl  13384  ge0xaddcl  13385  ge0xmulcl  13386  serge0  13968  expclzlem  13995  expge0  14010  expge1  14011  hashfacen  14357  hashfacenOLD  14358  wwlktovf1  14852  qredeu  16539  nn0gcdsq  16632  mul4sq  16831  fpwipodrs  18434  pwmnd  18752  gimco  19063  gictr  19070  symgextf1  19208  efgrelexlemb  19537  xrs1mnd  20851  lmimco  21266  lmictra  21267  cctop  22372  iscn2  22605  iscnp2  22606  paste  22661  txuni  22959  txcn  22993  txcmpb  23011  tx2ndc  23018  hmphtr  23150  snfil  23231  supfil  23262  filssufilg  23278  tsmsxp  23522  dscmet  23944  rlimcnp  26331  efnnfsumcl  26468  efchtdvds  26524  lgsne0  26699  mul2sq  26783  sltsolem1  27039  colinearalglem2  27898  nb3grprlem2  28371  cplgr3v  28425  crctcshwlkn0  28808  wwlksnextinj  28886  hsn0elch  30232  shscli  30301  hsupss  30325  5oalem6  30643  mdsldmd1i  31315  superpos  31338  bnj110  33527  msubco  34182  fnsingle  34550  funimage  34559  funpartfun  34574  bj-nnfan  35259  bj-nnfor  35261  bj-snsetex  35480  bj-snmoore  35630  difunieq  35891  riscer  36493  divrngidl  36533  rimco  40744  rictr  40747  nn0rppwr  40862  nn0expgcd  40864  dvdsexpnn0  40870  zaddcom  40964  zmulcom  40968  mzpincl  41100  kelac2lem  41434  omcl3g  41712  cllem0  41926  unhe1  42145  tz6.12-1-afv  45492  tz6.12-1-afv2  45559  sprsymrelf1  45774  prmdvdsfmtnof1lem2  45863  uspgrsprf1  46135  2zrngamgm  46323  2zrngmmgm  46330  rrx2xpref1o  46890  f1omo  47013
  Copyright terms: Public domain W3C validator