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  1372  imainss  4962  xpexr2m  4988  funeu2  5157  imadiflem  5210  fnop  5234  ssimaex  5490  isosolem  5733  acexmidlem2  5779  fnovex  5812  cnvoprab  6139  smores3  6198  freccllem  6307  riinerm  6510  enq0sym  7264  peano5nnnn  7724  axcaucvglemres  7731  uzind3  9188  xrltnsym  9609  xsubge0  9694  0fz1  9856  seqf  10265  seq3f1oleml  10307  exp1  10330  expp1  10331  resqrexlemf1  10812  resqrexlemfp1  10813  clim2ser  11138  clim2ser2  11139  isermulc2  11141  summodclem3  11181  fisumss  11193  fsum3cvg3  11197  iserabs  11276  isumshft  11291  isumsplit  11292  geoisum1  11320  geoisum1c  11321  cvgratnnlemnexp  11325  cvgratz  11333  mertenslem2  11337  clim2prod  11340  clim2divap  11341  fprodseq  11384  effsumlt  11435  efgt1p  11439  gcd0id  11703  lcmgcd  11795  lcmdvds  11796  lcmid  11797  isprm2lem  11833  ennnfonelemjn  11951  neipsm  12362  xmetpsmet  12577  comet  12707  metrest  12714  expcncf  12800  exmid1stab  13368  cvgcmp2nlemabs  13402