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  1437  exmid1stab  4298  imainss  5152  xpexr2m  5178  funeu2  5352  imadiflem  5409  fnop  5435  ssimaex  5707  isosolem  5965  acexmidlem2  6015  fnovex  6051  cnvoprab  6399  smores3  6459  freccllem  6568  riinerm  6777  pw1fin  7102  enq0sym  7652  peano5nnnn  8112  axcaucvglemres  8119  uzind3  9593  xrltnsym  10028  xsubge0  10116  0fz1  10280  seqf  10727  seq3f1oleml  10779  exp1  10808  expp1  10809  resqrexlemf1  11586  resqrexlemfp1  11587  clim2ser  11915  clim2ser2  11916  isermulc2  11918  summodclem3  11959  fisumss  11971  fsum3cvg3  11975  iserabs  12054  isumshft  12069  isumsplit  12070  geoisum1  12098  geoisum1c  12099  cvgratnnlemnexp  12103  cvgratz  12111  mertenslem2  12115  clim2prod  12118  clim2divap  12119  fprodseq  12162  prodssdc  12168  fprodssdc  12169  effsumlt  12271  efgt1p  12275  gcd0id  12568  nninfctlemfo  12629  lcmgcd  12668  lcmdvds  12669  lcmid  12670  isprm2lem  12706  pcmpt  12934  ennnfonelemjn  13041  issgrpd  13513  mulg1  13734  srglmhm  14025  srgrmhm  14026  ringlghm  14093  ringrghm  14094  neipsm  14897  xmetpsmet  15112  comet  15242  metrest  15249  expcncf  15352  lgscllem  15755  lgsdir2  15781  lgsdirnn0  15795  lgsdinn0  15796  eupth2lem3lem7fi  16344  cvgcmp2nlemabs  16687  nconstwlpolem  16721  gfsumval  16732