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  1393  exmid1stab  4208  imainss  5044  xpexr2m  5070  funeu2  5242  imadiflem  5295  fnop  5319  ssimaex  5577  isosolem  5824  acexmidlem2  5871  fnovex  5907  cnvoprab  6234  smores3  6293  freccllem  6402  riinerm  6607  pw1fin  6909  enq0sym  7430  peano5nnnn  7890  axcaucvglemres  7897  uzind3  9364  xrltnsym  9791  xsubge0  9879  0fz1  10042  seqf  10458  seq3f1oleml  10500  exp1  10523  expp1  10524  resqrexlemf1  11012  resqrexlemfp1  11013  clim2ser  11340  clim2ser2  11341  isermulc2  11343  summodclem3  11383  fisumss  11395  fsum3cvg3  11399  iserabs  11478  isumshft  11493  isumsplit  11494  geoisum1  11522  geoisum1c  11523  cvgratnnlemnexp  11527  cvgratz  11535  mertenslem2  11539  clim2prod  11542  clim2divap  11543  fprodseq  11586  prodssdc  11592  fprodssdc  11593  effsumlt  11695  efgt1p  11699  gcd0id  11974  lcmgcd  12072  lcmdvds  12073  lcmid  12074  isprm2lem  12110  pcmpt  12335  ennnfonelemjn  12397  mulg1  12944  srglmhm  13129  srgrmhm  13130  neipsm  13547  xmetpsmet  13762  comet  13892  metrest  13899  expcncf  13985  lgscllem  14301  lgsdir2  14327  lgsdirnn0  14341  lgsdinn0  14342  cvgcmp2nlemabs  14662  nconstwlpolem  14694