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  4237  imainss  5081  xpexr2m  5107  funeu2  5280  imadiflem  5333  fnop  5357  ssimaex  5618  isosolem  5867  acexmidlem2  5915  fnovex  5951  cnvoprab  6287  smores3  6346  freccllem  6455  riinerm  6662  pw1fin  6966  enq0sym  7492  peano5nnnn  7952  axcaucvglemres  7959  uzind3  9430  xrltnsym  9859  xsubge0  9947  0fz1  10111  seqf  10535  seq3f1oleml  10587  exp1  10616  expp1  10617  resqrexlemf1  11152  resqrexlemfp1  11153  clim2ser  11480  clim2ser2  11481  isermulc2  11483  summodclem3  11523  fisumss  11535  fsum3cvg3  11539  iserabs  11618  isumshft  11633  isumsplit  11634  geoisum1  11662  geoisum1c  11663  cvgratnnlemnexp  11667  cvgratz  11675  mertenslem2  11679  clim2prod  11682  clim2divap  11683  fprodseq  11726  prodssdc  11732  fprodssdc  11733  effsumlt  11835  efgt1p  11839  gcd0id  12116  nninfctlemfo  12177  lcmgcd  12216  lcmdvds  12217  lcmid  12218  isprm2lem  12254  pcmpt  12481  ennnfonelemjn  12559  issgrpd  12995  mulg1  13199  srglmhm  13489  srgrmhm  13490  ringlghm  13557  ringrghm  13558  neipsm  14322  xmetpsmet  14537  comet  14667  metrest  14674  expcncf  14763  lgscllem  15123  lgsdir2  15149  lgsdirnn0  15163  lgsdinn0  15164  cvgcmp2nlemabs  15522  nconstwlpolem  15555