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

Theorem sylan2br 284
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
sylan2br.1 (𝜒𝜑)
sylan2br.2 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
sylan2br ((𝜓𝜑) → 𝜃)

Proof of Theorem sylan2br
StepHypRef Expression
1 sylan2br.1 . . 3 (𝜒𝜑)
21biimpri 132 . 2 (𝜑𝜒)
3 sylan2br.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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  syl2anbr  288  xordc1  1339  imainss  4890  xpexr2m  4916  funeu2  5085  imadiflem  5138  fnop  5162  ssimaex  5414  isosolem  5657  acexmidlem2  5703  fnovex  5736  cnvoprab  6061  smores3  6120  freccllem  6229  riinerm  6432  enq0sym  7141  peano5nnnn  7577  axcaucvglemres  7584  uzind3  9016  xrltnsym  9420  xsubge0  9505  0fz1  9666  seqf  10075  seq3f1oleml  10117  exp1  10140  expp1  10141  resqrexlemf1  10620  resqrexlemfp1  10621  clim2ser  10945  clim2ser2  10946  isermulc2  10948  summodclem3  10988  fisumss  11000  fsum3cvg3  11004  iserabs  11083  isumshft  11098  isumsplit  11099  geoisum1  11127  geoisum1c  11128  cvgratnnlemnexp  11132  cvgratz  11140  mertenslem2  11144  effsumlt  11196  efgt1p  11200  gcd0id  11462  lcmgcd  11552  lcmdvds  11553  lcmid  11554  isprm2lem  11590  ennnfonelemjn  11707  neipsm  12105  xmetpsmet  12297  comet  12427  metrest  12434  expcncf  12504  cvgcmp2nlemabs  12811
  Copyright terms: Public domain W3C validator