Theorem sylan2br 286

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 284	1 |- ( ( ps /\ ph ) -> th )

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  7240  peano5nnnn  7700  axcaucvglemres  7707  uzind3  9164  xrltnsym  9579  xsubge0  9664  0fz1  9825  seqf  10234  seq3f1oleml  10276  exp1  10299  expp1  10300  resqrexlemf1  10780  resqrexlemfp1  10781  clim2ser  11106  clim2ser2  11107  isermulc2  11109  summodclem3  11149  fisumss  11161  fsum3cvg3  11165  iserabs  11244  isumshft  11259  isumsplit  11260  geoisum1  11288  geoisum1c  11289  cvgratnnlemnexp  11293  cvgratz  11301  mertenslem2  11305  clim2prod  11308  clim2divap  11309  effsumlt  11398  efgt1p  11402  gcd0id  11667  lcmgcd  11759  lcmdvds  11760  lcmid  11761  isprm2lem  11797  ennnfonelemjn  11915  neipsm  12323  xmetpsmet  12538  comet  12668  metrest  12675  expcncf  12761  exmid1stab  13195  cvgcmp2nlemabs  13227