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  1413  exmid1stab  4253  imainss  5099  xpexr2m  5125  funeu2  5298  imadiflem  5354  fnop  5380  ssimaex  5642  isosolem  5895  acexmidlem2  5943  fnovex  5979  cnvoprab  6322  smores3  6381  freccllem  6490  riinerm  6697  pw1fin  7009  enq0sym  7547  peano5nnnn  8007  axcaucvglemres  8014  uzind3  9488  xrltnsym  9917  xsubge0  10005  0fz1  10169  seqf  10611  seq3f1oleml  10663  exp1  10692  expp1  10693  resqrexlemf1  11352  resqrexlemfp1  11353  clim2ser  11681  clim2ser2  11682  isermulc2  11684  summodclem3  11724  fisumss  11736  fsum3cvg3  11740  iserabs  11819  isumshft  11834  isumsplit  11835  geoisum1  11863  geoisum1c  11864  cvgratnnlemnexp  11868  cvgratz  11876  mertenslem2  11880  clim2prod  11883  clim2divap  11884  fprodseq  11927  prodssdc  11933  fprodssdc  11934  effsumlt  12036  efgt1p  12040  gcd0id  12333  nninfctlemfo  12394  lcmgcd  12433  lcmdvds  12434  lcmid  12435  isprm2lem  12471  pcmpt  12699  ennnfonelemjn  12806  issgrpd  13277  mulg1  13498  srglmhm  13788  srgrmhm  13789  ringlghm  13856  ringrghm  13857  neipsm  14659  xmetpsmet  14874  comet  15004  metrest  15011  expcncf  15114  lgscllem  15517  lgsdir2  15543  lgsdirnn0  15557  lgsdinn0  15558  cvgcmp2nlemabs  16008  nconstwlpolem  16041