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  1371  imainss  4954  xpexr2m  4980  funeu2  5149  imadiflem  5202  fnop  5226  ssimaex  5482  isosolem  5725  acexmidlem2  5771  fnovex  5804  cnvoprab  6131  smores3  6190  freccllem  6299  riinerm  6502  enq0sym  7254  peano5nnnn  7714  axcaucvglemres  7721  uzind3  9178  xrltnsym  9593  xsubge0  9678  0fz1  9839  seqf  10248  seq3f1oleml  10290  exp1  10313  expp1  10314  resqrexlemf1  10794  resqrexlemfp1  10795  clim2ser  11120  clim2ser2  11121  isermulc2  11123  summodclem3  11163  fisumss  11175  fsum3cvg3  11179  iserabs  11258  isumshft  11273  isumsplit  11274  geoisum1  11302  geoisum1c  11303  cvgratnnlemnexp  11307  cvgratz  11315  mertenslem2  11319  clim2prod  11322  clim2divap  11323  effsumlt  11412  efgt1p  11416  gcd0id  11680  lcmgcd  11772  lcmdvds  11773  lcmid  11774  isprm2lem  11810  ennnfonelemjn  11928  neipsm  12339  xmetpsmet  12554  comet  12684  metrest  12691  expcncf  12777  exmid1stab  13302  cvgcmp2nlemabs  13336
  Copyright terms: Public domain W3C validator