Theorem sylan2br 283

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

Step	Hyp	Ref	Expression
1		sylan2br.1	. . 3 |- ( ch <-> ph )
2	1	biimpri 132	. 2 |- ( ph -> ch )
3		sylan2br.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 281	1 |- ( ( ps /\ ph ) -> th )

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  287  xordc1  1330  imainss  4860  xpexr2m  4885  funeu2  5054  imadiflem  5106  fnop  5130  ssimaex  5378  isosolem  5617  acexmidlem2  5663  fnovex  5696  cnvoprab  6013  smores3  6072  freccllem  6181  riinerm  6379  enq0sym  7052  peano5nnnn  7488  axcaucvglemres  7495  uzind3  8920  xrltnsym  9324  0fz1  9520  iseqfcl  9939  iseqfclt  9940  seqf  9941  seq3f1oleml  9993  exp1  10022  expp1  10023  resqrexlemf1  10502  resqrexlemfp1  10503  clim2ser  10786  clim2ser2  10787  iisermulc2  10789  isermulc2  10790  isummolem3  10831  isum  10837  fisumss  10845  fsum3cvg3  10850  isumclim  10876  iserabs  10930  isumshft  10945  isumsplit  10946  geoisum1  10974  geoisum1c  10975  cvgratnnlemnexp  10979  cvgratz  10987  mertenslem2  10991  effsumlt  11043  efgt1p  11047  gcd0id  11309  lcmgcd  11399  lcmdvds  11400  lcmid  11401  isprm2lem  11437