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  1375  imainss  5001  xpexr2m  5027  funeu2  5196  imadiflem  5249  fnop  5273  ssimaex  5529  isosolem  5774  acexmidlem2  5821  fnovex  5854  cnvoprab  6181  smores3  6240  freccllem  6349  riinerm  6553  pw1fin  6855  enq0sym  7352  peano5nnnn  7812  axcaucvglemres  7819  uzind3  9277  xrltnsym  9700  xsubge0  9785  0fz1  9947  seqf  10360  seq3f1oleml  10402  exp1  10425  expp1  10426  resqrexlemf1  10908  resqrexlemfp1  10909  clim2ser  11234  clim2ser2  11235  isermulc2  11237  summodclem3  11277  fisumss  11289  fsum3cvg3  11293  iserabs  11372  isumshft  11387  isumsplit  11388  geoisum1  11416  geoisum1c  11417  cvgratnnlemnexp  11421  cvgratz  11429  mertenslem2  11433  clim2prod  11436  clim2divap  11437  fprodseq  11480  prodssdc  11486  fprodssdc  11487  effsumlt  11589  efgt1p  11593  gcd0id  11862  lcmgcd  11954  lcmdvds  11955  lcmid  11956  isprm2lem  11992  ennnfonelemjn  12131  neipsm  12554  xmetpsmet  12769  comet  12899  metrest  12906  expcncf  12992  exmid1stab  13572  cvgcmp2nlemabs  13603  nconstwlpolem  13635