ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylan2b 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  843  bm1.1  2025  eqtr3  2059  morex  2725  reuss2  3217  reupick  3221  rabsneu  3443  opabss  3821  triun  3867  poirr  4044  wepo  4096  wetrep  4097  rexxfrd  4195  reg3exmidlemwe  4303  nnsuc  4338  fnfco  5065  fun11iun  5147  fnressn  5349  fvpr1g  5367  fvtp1g  5369  fvtp3g  5371  fvtp3  5374  f1mpt  5410  caovlem2d  5693  offval  5719  dfoprab3  5817  1stconst  5842  2ndconst  5843  poxp  5853  tfrlemisucaccv  5939  addclpi  6423  addnidpig  6432  reapmul1  7584  nnnn0addcl  8210  un0addcl  8213  un0mulcl  8214  zltnle  8289  nn0ge0div  8325  uzind3  8349  uzind4  8529  ltsubrp  8615  ltaddrp  8616  xrlttr  8714  xrltso  8715  xltnegi  8746  fzind2  9093  qltnle  9099  expp1  9236  expnegap0  9237  expcllem  9240  mulexpzap  9269  expaddzap  9273  expmulzap  9275  shftf  9405  sqrtdiv  9614  mulcn2  9807  ialgrf  9858  bj-bdfindes  10048  bj-findes  10080
  Copyright terms: Public domain W3C validator