Theorem sylan2br 282

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 131	. 2 |- ( ph -> ch )
3		sylan2br.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 280	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  syl2anbr  286  xordc1  1324  imainss  4759  xpexr2m  4782  funeu2  4947  imadiflem  4998  fnop  5022  ssimaex  5255  isosolem  5483  acexmidlem2  5529  fnovex  5558  cnvoprab  5875  smores3  5931  riinerm  6202  enq0sym  6622  peano5nnnn  7058  axcaucvglemres  7065  uzind3  8460  xrltnsym  8868  0fz1  9064  iseqf  9444  expivallem  9477  expival  9478  exp1  9482  expp1  9483  resqrexlemf1  9894  resqrexlemfp1  9895  clim2iser  10175  clim2iser2  10176  iisermulc2  10178  iserile  10180  climserile  10183  gcd0id  10370  lcmgcd  10460  lcmdvds  10461  lcmid  10462  isprm2lem  10498