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  1435  exmid1stab  4292  imainss  5144  xpexr2m  5170  funeu2  5344  imadiflem  5400  fnop  5426  ssimaex  5697  isosolem  5954  acexmidlem2  6004  fnovex  6040  cnvoprab  6386  smores3  6445  freccllem  6554  riinerm  6763  pw1fin  7083  enq0sym  7630  peano5nnnn  8090  axcaucvglemres  8097  uzind3  9571  xrltnsym  10001  xsubge0  10089  0fz1  10253  seqf  10698  seq3f1oleml  10750  exp1  10779  expp1  10780  resqrexlemf1  11535  resqrexlemfp1  11536  clim2ser  11864  clim2ser2  11865  isermulc2  11867  summodclem3  11907  fisumss  11919  fsum3cvg3  11923  iserabs  12002  isumshft  12017  isumsplit  12018  geoisum1  12046  geoisum1c  12047  cvgratnnlemnexp  12051  cvgratz  12059  mertenslem2  12063  clim2prod  12066  clim2divap  12067  fprodseq  12110  prodssdc  12116  fprodssdc  12117  effsumlt  12219  efgt1p  12223  gcd0id  12516  nninfctlemfo  12577  lcmgcd  12616  lcmdvds  12617  lcmid  12618  isprm2lem  12654  pcmpt  12882  ennnfonelemjn  12989  issgrpd  13461  mulg1  13682  srglmhm  13972  srgrmhm  13973  ringlghm  14040  ringrghm  14041  neipsm  14844  xmetpsmet  15059  comet  15189  metrest  15196  expcncf  15299  lgscllem  15702  lgsdir2  15728  lgsdirnn0  15742  lgsdinn0  15743  cvgcmp2nlemabs  16488  nconstwlpolem  16521