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  7379  nnnn0addcl  7988  un0addcl  7991  un0mulcl  7992  zltnle  8067  nn0ge0div  8103  uzind3  8127  uzind4  8307  ltsubrp  8392  ltaddrp  8393  xrlttr  8486  xrltso  8487  xltnegi  8518  fzind2  8865  expp1  8916  expnegap0  8917  expcllem  8920  mulexpzap  8949  expaddzap  8953  expmulzap  8955  bj-bdfindes  9409  bj-findes  9441
  Copyright terms: Public domain W3C validator