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  4209  imainss  5045  xpexr2m  5071  funeu2  5243  imadiflem  5296  fnop  5320  ssimaex  5578  isosolem  5825  acexmidlem2  5872  fnovex  5908  cnvoprab  6235  smores3  6294  freccllem  6403  riinerm  6608  pw1fin  6910  enq0sym  7431  peano5nnnn  7891  axcaucvglemres  7898  uzind3  9366  xrltnsym  9793  xsubge0  9881  0fz1  10045  seqf  10461  seq3f1oleml  10503  exp1  10526  expp1  10527  resqrexlemf1  11017  resqrexlemfp1  11018  clim2ser  11345  clim2ser2  11346  isermulc2  11348  summodclem3  11388  fisumss  11400  fsum3cvg3  11404  iserabs  11483  isumshft  11498  isumsplit  11499  geoisum1  11527  geoisum1c  11528  cvgratnnlemnexp  11532  cvgratz  11540  mertenslem2  11544  clim2prod  11547  clim2divap  11548  fprodseq  11591  prodssdc  11597  fprodssdc  11598  effsumlt  11700  efgt1p  11704  gcd0id  11980  lcmgcd  12078  lcmdvds  12079  lcmid  12080  isprm2lem  12116  pcmpt  12341  ennnfonelemjn  12403  mulg1  12990  srglmhm  13176  srgrmhm  13177  neipsm  13657  xmetpsmet  13872  comet  14002  metrest  14009  expcncf  14095  lgscllem  14411  lgsdir2  14437  lgsdirnn0  14451  lgsdinn0  14452  cvgcmp2nlemabs  14783  nconstwlpolem  14815