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

Theorem sylan2b 281
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 118 . 2 (𝜑𝜒)
3 sylan2b.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan2 280 1 ((𝜓𝜑) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  syl2anb  285  dcor  879  bm1.1  2070  eqtr3  2104  morex  2790  reuss2  3268  reupick  3272  rabsneu  3498  opabss  3877  triun  3924  poirr  4108  wepo  4160  wetrep  4161  rexxfrd  4259  reg3exmidlemwe  4367  nnsuc  4403  fnfco  5149  fun11iun  5237  fnressn  5446  fvpr1g  5464  fvtp1g  5466  fvtp3g  5468  fvtp3  5471  f1mpt  5511  caovlem2d  5794  offval  5820  dfoprab3  5918  1stconst  5943  2ndconst  5944  poxp  5954  tfrlemisucaccv  6044  tfr1onlemsucaccv  6060  tfrcllemsucaccv  6073  addclpi  6830  addnidpig  6839  reapmul1  8013  nnnn0addcl  8636  un0addcl  8639  un0mulcl  8640  zltnle  8729  nn0ge0div  8766  uzind3  8792  uzind4  9008  ltsubrp  9100  ltaddrp  9101  xrlttr  9197  xrltso  9198  xltnegi  9229  fzind2  9578  qltnle  9585  qbtwnxr  9597  expp1  9861  expnegap0  9862  expcllem  9865  mulexpzap  9894  expaddzap  9898  expmulzap  9900  hashunlem  10109  shftf  10161  sqrtdiv  10371  mulcn2  10595  isummolem2  10663  dvdsflip  10734  dvdsfac  10743  ialgrf  10909  lcmgcdlem  10941  rpexp1i  11015  hashdvds  11079  hashgcdlem  11085  bj-bdfindes  11289  bj-findes  11321
  Copyright terms: Public domain W3C validator