Theorem sylan2br 288

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl2anbr  292  xordc1  1404  exmid1stab  4242  imainss  5086  xpexr2m  5112  funeu2  5285  imadiflem  5338  fnop  5364  ssimaex  5625  isosolem  5874  acexmidlem2  5922  fnovex  5958  cnvoprab  6301  smores3  6360  freccllem  6469  riinerm  6676  pw1fin  6980  enq0sym  7516  peano5nnnn  7976  axcaucvglemres  7983  uzind3  9456  xrltnsym  9885  xsubge0  9973  0fz1  10137  seqf  10573  seq3f1oleml  10625  exp1  10654  expp1  10655  resqrexlemf1  11190  resqrexlemfp1  11191  clim2ser  11519  clim2ser2  11520  isermulc2  11522  summodclem3  11562  fisumss  11574  fsum3cvg3  11578  iserabs  11657  isumshft  11672  isumsplit  11673  geoisum1  11701  geoisum1c  11702  cvgratnnlemnexp  11706  cvgratz  11714  mertenslem2  11718  clim2prod  11721  clim2divap  11722  fprodseq  11765  prodssdc  11771  fprodssdc  11772  effsumlt  11874  efgt1p  11878  gcd0id  12171  nninfctlemfo  12232  lcmgcd  12271  lcmdvds  12272  lcmid  12273  isprm2lem  12309  pcmpt  12537  ennnfonelemjn  12644  issgrpd  13114  mulg1  13335  srglmhm  13625  srgrmhm  13626  ringlghm  13693  ringrghm  13694  neipsm  14474  xmetpsmet  14689  comet  14819  metrest  14826  expcncf  14929  lgscllem  15332  lgsdir2  15358  lgsdirnn0  15372  lgsdinn0  15373  cvgcmp2nlemabs  15763  nconstwlpolem  15796