Theorem sylan2br 286

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anbr  290  xordc1  1388  imainss  5026  xpexr2m  5052  funeu2  5224  imadiflem  5277  fnop  5301  ssimaex  5557  isosolem  5803  acexmidlem2  5850  fnovex  5886  cnvoprab  6213  smores3  6272  freccllem  6381  riinerm  6586  pw1fin  6888  enq0sym  7394  peano5nnnn  7854  axcaucvglemres  7861  uzind3  9325  xrltnsym  9750  xsubge0  9838  0fz1  10001  seqf  10417  seq3f1oleml  10459  exp1  10482  expp1  10483  resqrexlemf1  10972  resqrexlemfp1  10973  clim2ser  11300  clim2ser2  11301  isermulc2  11303  summodclem3  11343  fisumss  11355  fsum3cvg3  11359  iserabs  11438  isumshft  11453  isumsplit  11454  geoisum1  11482  geoisum1c  11483  cvgratnnlemnexp  11487  cvgratz  11495  mertenslem2  11499  clim2prod  11502  clim2divap  11503  fprodseq  11546  prodssdc  11552  fprodssdc  11553  effsumlt  11655  efgt1p  11659  gcd0id  11934  lcmgcd  12032  lcmdvds  12033  lcmid  12034  isprm2lem  12070  pcmpt  12295  ennnfonelemjn  12357  neipsm  12948  xmetpsmet  13163  comet  13293  metrest  13300  expcncf  13386  lgscllem  13702  lgsdir2  13728  lgsdirnn0  13742  lgsdinn0  13743  exmid1stab  14033  cvgcmp2nlemabs  14064  nconstwlpolem  14096