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

Theorem sylan2b 271
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
sylan2b.1 (φχ)
sylan2b.2 ((ψ χ) → θ)
Assertion
Ref Expression
sylan2b ((ψ φ) → θ)

Proof of Theorem sylan2b
StepHypRef Expression
1 sylan2b.1 . . 3 (φχ)
21biimpi 113 . 2 (φχ)
3 sylan2b.2 . 2 ((ψ χ) → θ)
42, 3sylan2 270 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:  syl2anb  275  dcor  842  bm1.1  2022  eqtr3  2056  morex  2719  reuss2  3211  reupick  3215  rabsneu  3434  opabss  3812  triun  3858  poirr  4035  rexxfrd  4161  nnsuc  4281  fnfco  5008  fun11iun  5090  fnressn  5292  fvpr1g  5310  fvtp1g  5312  fvtp3g  5314  fvtp3  5317  f1mpt  5353  caovlem2d  5635  offval  5661  dfoprab3  5759  1stconst  5784  2ndconst  5785  poxp  5794  tfrlemisucaccv  5880  addclpi  6311  addnidpig  6320  reapmul1  7359  nnnn0addcl  7968  un0addcl  7971  un0mulcl  7972  zltnle  8047  nn0ge0div  8083  uzind3  8107  uzind4  8287  ltsubrp  8372  ltaddrp  8373  xrlttr  8466  xrltso  8467  xltnegi  8498  fzind2  8845  expp1  8896  expnegap0  8897  expcllem  8900  mulexpzap  8929  expaddzap  8933  expmulzap  8935  bj-bdfindes  9383  bj-findes  9411
  Copyright terms: Public domain W3C validator