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  1438  exmid1stab  4304  imainss  5159  xpexr2m  5185  funeu2  5359  imadiflem  5416  fnop  5442  ssimaex  5716  isosolem  5975  acexmidlem2  6025  fnovex  6061  cnvoprab  6408  suppssdc  6438  smores3  6502  freccllem  6611  riinerm  6820  pw1fin  7145  enq0sym  7712  peano5nnnn  8172  axcaucvglemres  8179  uzind3  9654  xrltnsym  10089  xsubge0  10177  0fz1  10342  seqf  10789  seq3f1oleml  10841  exp1  10870  expp1  10871  resqrexlemf1  11648  resqrexlemfp1  11649  clim2ser  11977  clim2ser2  11978  isermulc2  11980  summodclem3  12021  fisumss  12033  fsum3cvg3  12037  iserabs  12116  isumshft  12131  isumsplit  12132  geoisum1  12160  geoisum1c  12161  cvgratnnlemnexp  12165  cvgratz  12173  mertenslem2  12177  clim2prod  12180  clim2divap  12181  fprodseq  12224  prodssdc  12230  fprodssdc  12231  effsumlt  12333  efgt1p  12337  gcd0id  12630  nninfctlemfo  12691  lcmgcd  12730  lcmdvds  12731  lcmid  12732  isprm2lem  12768  pcmpt  12996  ennnfonelemjn  13103  issgrpd  13575  mulg1  13796  srglmhm  14087  srgrmhm  14088  ringlghm  14155  ringrghm  14156  neipsm  14965  xmetpsmet  15180  comet  15310  metrest  15317  expcncf  15420  lgscllem  15826  lgsdir2  15852  lgsdirnn0  15866  lgsdinn0  15867  eupth2lem3lem7fi  16415  cvgcmp2nlemabs  16764  nconstwlpolem  16798  gfsumval  16809