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  877  bm1.1  2067  eqtr3  2101  morex  2777  reuss2  3245  reupick  3249  rabsneu  3467  opabss  3844  triun  3890  poirr  4064  wepo  4116  wetrep  4117  rexxfrd  4215  reg3exmidlemwe  4323  nnsuc  4358  fnfco  5090  fun11iun  5172  fnressn  5375  fvpr1g  5393  fvtp1g  5395  fvtp3g  5397  fvtp3  5400  f1mpt  5436  caovlem2d  5718  offval  5744  dfoprab3  5842  1stconst  5867  2ndconst  5868  poxp  5878  tfrlemisucaccv  5968  tfr1onlemsucaccv  5984  tfrcllemsucaccv  5997  addclpi  6568  addnidpig  6577  reapmul1  7751  nnnn0addcl  8374  un0addcl  8377  un0mulcl  8378  zltnle  8467  nn0ge0div  8504  uzind3  8530  uzind4  8746  ltsubrp  8838  ltaddrp  8839  xrlttr  8935  xrltso  8936  xltnegi  8967  fzind2  9314  qltnle  9321  qbtwnxr  9333  expp1  9569  expnegap0  9570  expcllem  9573  mulexpzap  9602  expaddzap  9606  expmulzap  9608  sizeunlem  9817  shftf  9845  sqrtdiv  10055  mulcn2  10278  dvdsflip  10385  dvdsfac  10394  ialgrf  10560  lcmgcdlem  10592  rpexp1i  10666  bj-bdfindes  10887  bj-findes  10919
  Copyright terms: Public domain W3C validator