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

Theorem sylan2br 272
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
sylan2br.1  |-  ( ch  <->  ph )
sylan2br.2  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
sylan2br  |-  ( ( ps  /\  ph )  ->  th )

Proof of Theorem sylan2br
StepHypRef Expression
1 sylan2br.1 . . 3  |-  ( ch  <->  ph )
21biimpri 124 . 2  |-  ( ph  ->  ch )
3 sylan2br.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan2 270 1  |-  ( ( ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  syl2anbr  276  xordc1  1284  imainss  4739  xpexr2m  4762  funeu2  4927  imadiflem  4978  fnop  5002  ssimaex  5234  isosolem  5463  acexmidlem2  5509  fnovex  5538  smores3  5908  riinerm  6179  enq0sym  6530  peano5nnnn  6966  axcaucvglemres  6973  uzind3  8351  xrltnsym  8714  0fz1  8909  iseqf  9224  expivallem  9256  expival  9257  exp1  9261  expp1  9262  resqrexlemf1  9606  resqrexlemfp1  9607  clim2iser  9857  clim2iser2  9858  iisermulc2  9860  iserile  9862  climserile  9865
  Copyright terms: Public domain W3C validator