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

Theorem sylan2br 286
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 284 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:  syl2anbr  290  xordc1  1356  imainss  4924  xpexr2m  4950  funeu2  5119  imadiflem  5172  fnop  5196  ssimaex  5450  isosolem  5693  acexmidlem2  5739  fnovex  5772  cnvoprab  6099  smores3  6158  freccllem  6267  riinerm  6470  enq0sym  7208  peano5nnnn  7668  axcaucvglemres  7675  uzind3  9132  xrltnsym  9547  xsubge0  9632  0fz1  9793  seqf  10202  seq3f1oleml  10244  exp1  10267  expp1  10268  resqrexlemf1  10748  resqrexlemfp1  10749  clim2ser  11074  clim2ser2  11075  isermulc2  11077  summodclem3  11117  fisumss  11129  fsum3cvg3  11133  iserabs  11212  isumshft  11227  isumsplit  11228  geoisum1  11256  geoisum1c  11257  cvgratnnlemnexp  11261  cvgratz  11269  mertenslem2  11273  effsumlt  11325  efgt1p  11329  gcd0id  11594  lcmgcd  11686  lcmdvds  11687  lcmid  11688  isprm2lem  11724  ennnfonelemjn  11842  neipsm  12250  xmetpsmet  12465  comet  12595  metrest  12602  expcncf  12688  exmid1stab  13122  cvgcmp2nlemabs  13154
  Copyright terms: Public domain W3C validator