ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2anb Structured version   GIF version

Theorem syl2anb 275
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 268 . 2 ((φ χ) → θ)
51, 4sylan2b 271 1 ((φ τ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  sylancb  395  reupick3  3216  difprsnss  3493  trin2  4659  imadiflem  4921  fnun  4948  fco  4999  f1co  5044  foco  5059  f1oun  5089  f1oco  5092  eqfunfv  5213  ftpg  5290  issmo  5844  tfrlem5  5871  ener  6195  domtr  6201  unen  6229  xpdom2  6241  axpre-lttrn  6748  axpre-mulgt0  6751  zmulcl  8053  qaddcl  8326  qmulcl  8328  rpaddcl  8361  rpmulcl  8362  rpdivcl  8363  xrltnsym  8464  xrlttri3  8468  ge0addcl  8600  ge0mulcl  8601  expclzaplem  8913  expge0  8925  expge1  8926
  Copyright terms: Public domain W3C validator