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

Theorem sylan2b 283
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 119 . 2 (𝜑𝜒)
3 sylan2b.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3sylan2 282 1 ((𝜓𝜑) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  syl2anb  287  dcor  902  bm1.1  2100  eqtr3  2135  elnelne1  2387  elnelne2  2388  morex  2839  reuss2  3324  reupick  3328  rabsneu  3564  opabss  3960  triun  4007  poirr  4197  wepo  4249  wetrep  4250  rexxfrd  4352  reg3exmidlemwe  4461  nnsuc  4497  fnfco  5265  fun11iun  5354  fnressn  5572  fvpr1g  5592  fvtp1g  5594  fvtp3g  5596  fvtp3  5599  f1mpt  5638  caovlem2d  5929  offval  5955  dfoprab3  6055  1stconst  6084  2ndconst  6085  poxp  6095  tfrlemisucaccv  6188  tfr1onlemsucaccv  6204  tfrcllemsucaccv  6217  fiintim  6783  addclpi  7099  addnidpig  7108  reapmul1  8320  nnnn0addcl  8958  un0addcl  8961  un0mulcl  8962  zltnle  9051  nn0ge0div  9089  uzind3  9115  uzind4  9332  ltsubrp  9424  ltaddrp  9425  xrlttr  9521  xrltso  9522  xltnegi  9558  xaddnemnf  9580  xaddnepnf  9581  xaddcom  9584  xnegdi  9591  xsubge0  9604  fzind2  9956  qltnle  9963  qbtwnxr  9975  exp3vallem  10234  expp1  10240  expnegap0  10241  expcllem  10244  mulexpzap  10273  expaddzap  10277  expmulzap  10279  hashunlem  10490  shftf  10542  sqrtdiv  10754  mulcn2  11021  summodclem2  11091  fsum3  11096  cvgratz  11241  dvdsflip  11445  dvdsfac  11454  lcmgcdlem  11654  rpexp1i  11728  hashdvds  11792  hashgcdlem  11798  lmss  12310  xmetrtri  12440  blssioo  12609  divcnap  12619  dvidlemap  12712  dvrecap  12729  dveflem  12738  bj-bdfindes  12958  bj-findes  12990
  Copyright terms: Public domain W3C validator