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  1438  exmid1stab  4323  imainss  5180  xpexr2m  5206  funeu2  5380  imadiflem  5437  fnop  5463  ssimaex  5740  isosolem  5999  acexmidlem2  6049  fnovex  6085  cnvoprab  6432  suppssdc  6462  smores3  6526  freccllem  6635  riinerm  6844  pw1fin  7172  enq0sym  7749  peano5nnnn  8209  axcaucvglemres  8216  uzind3  9694  xrltnsym  10129  xsubge0  10217  0fz1  10382  seqf  10830  seq3f1oleml  10882  exp1  10911  expp1  10912  resqrexlemf1  11697  resqrexlemfp1  11698  clim2ser  12026  clim2ser2  12027  isermulc2  12029  summodclem3  12070  fisumss  12082  fsum3cvg3  12086  iserabs  12165  isumshft  12180  isumsplit  12181  geoisum1  12209  geoisum1c  12210  cvgratnnlemnexp  12214  cvgratz  12222  mertenslem2  12226  clim2prod  12229  clim2divap  12230  fprodseq  12273  prodssdc  12279  fprodssdc  12280  effsumlt  12382  efgt1p  12386  gcd0id  12679  nninfctlemfo  12740  lcmgcd  12779  lcmdvds  12780  lcmid  12781  isprm2lem  12817  pcmpt  13045  ballotfilemfc0  13153  ballotfilemfcc  13154  ennnfonelemjn  13170  issgrpd  13642  mulg1  13863  srglmhm  14154  srgrmhm  14155  ringlghm  14222  ringrghm  14223  neipsm  15036  xmetpsmet  15251  comet  15381  metrest  15388  expcncf  15491  lgscllem  15897  lgsdir2  15923  lgsdirnn0  15937  lgsdinn0  15938  eupth2lem3lem7fi  16486  cvgcmp2nlemabs  16833  nconstwlpolem  16868  gfsumval  16879