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

Theorem sylan2br 284
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 132 . 2  |-  ( ph  ->  ch )
3 sylan2br.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan2 282 1  |-  ( ( ps  /\  ph )  ->  th )
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  288  xordc1  1354  imainss  4922  xpexr2m  4948  funeu2  5117  imadiflem  5170  fnop  5194  ssimaex  5448  isosolem  5691  acexmidlem2  5737  fnovex  5770  cnvoprab  6097  smores3  6156  freccllem  6265  riinerm  6468  enq0sym  7204  peano5nnnn  7664  axcaucvglemres  7671  uzind3  9118  xrltnsym  9530  xsubge0  9615  0fz1  9776  seqf  10185  seq3f1oleml  10227  exp1  10250  expp1  10251  resqrexlemf1  10731  resqrexlemfp1  10732  clim2ser  11057  clim2ser2  11058  isermulc2  11060  summodclem3  11100  fisumss  11112  fsum3cvg3  11116  iserabs  11195  isumshft  11210  isumsplit  11211  geoisum1  11239  geoisum1c  11240  cvgratnnlemnexp  11244  cvgratz  11252  mertenslem2  11256  effsumlt  11308  efgt1p  11312  gcd0id  11574  lcmgcd  11666  lcmdvds  11667  lcmid  11668  isprm2lem  11704  ennnfonelemjn  11821  neipsm  12229  xmetpsmet  12444  comet  12574  metrest  12581  expcncf  12667  exmid1stab  13029  cvgcmp2nlemabs  13061
  Copyright terms: Public domain W3C validator