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  4238  imainss  5082  xpexr2m  5108  funeu2  5281  imadiflem  5334  fnop  5358  ssimaex  5619  isosolem  5868  acexmidlem2  5916  fnovex  5952  cnvoprab  6289  smores3  6348  freccllem  6457  riinerm  6664  pw1fin  6968  enq0sym  7494  peano5nnnn  7954  axcaucvglemres  7961  uzind3  9433  xrltnsym  9862  xsubge0  9950  0fz1  10114  seqf  10538  seq3f1oleml  10590  exp1  10619  expp1  10620  resqrexlemf1  11155  resqrexlemfp1  11156  clim2ser  11483  clim2ser2  11484  isermulc2  11486  summodclem3  11526  fisumss  11538  fsum3cvg3  11542  iserabs  11621  isumshft  11636  isumsplit  11637  geoisum1  11665  geoisum1c  11666  cvgratnnlemnexp  11670  cvgratz  11678  mertenslem2  11682  clim2prod  11685  clim2divap  11686  fprodseq  11729  prodssdc  11735  fprodssdc  11736  effsumlt  11838  efgt1p  11842  gcd0id  12119  nninfctlemfo  12180  lcmgcd  12219  lcmdvds  12220  lcmid  12221  isprm2lem  12257  pcmpt  12484  ennnfonelemjn  12562  issgrpd  12998  mulg1  13202  srglmhm  13492  srgrmhm  13493  ringlghm  13560  ringrghm  13561  neipsm  14333  xmetpsmet  14548  comet  14678  metrest  14685  expcncf  14788  lgscllem  15164  lgsdir2  15190  lgsdirnn0  15204  lgsdinn0  15205  cvgcmp2nlemabs  15592  nconstwlpolem  15625