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  5695  isosolem  5948  acexmidlem2  5998  fnovex  6034  cnvoprab  6380  smores3  6439  freccllem  6548  riinerm  6755  pw1fin  7072  enq0sym  7619  peano5nnnn  8079  axcaucvglemres  8086  uzind3  9560  xrltnsym  9989  xsubge0  10077  0fz1  10241  seqf  10686  seq3f1oleml  10738  exp1  10767  expp1  10768  resqrexlemf1  11519  resqrexlemfp1  11520  clim2ser  11848  clim2ser2  11849  isermulc2  11851  summodclem3  11891  fisumss  11903  fsum3cvg3  11907  iserabs  11986  isumshft  12001  isumsplit  12002  geoisum1  12030  geoisum1c  12031  cvgratnnlemnexp  12035  cvgratz  12043  mertenslem2  12047  clim2prod  12050  clim2divap  12051  fprodseq  12094  prodssdc  12100  fprodssdc  12101  effsumlt  12203  efgt1p  12207  gcd0id  12500  nninfctlemfo  12561  lcmgcd  12600  lcmdvds  12601  lcmid  12602  isprm2lem  12638  pcmpt  12866  ennnfonelemjn  12973  issgrpd  13445  mulg1  13666  srglmhm  13956  srgrmhm  13957  ringlghm  14024  ringrghm  14025  neipsm  14828  xmetpsmet  15043  comet  15173  metrest  15180  expcncf  15283  lgscllem  15686  lgsdir2  15712  lgsdirnn0  15726  lgsdinn0  15727  cvgcmp2nlemabs  16400  nconstwlpolem  16433