Theorem sylan2br 286

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 132	. 2 |- ( ph -> ch )
3		sylan2br.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 284	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anbr  290  xordc1  1383  imainss  5019  xpexr2m  5045  funeu2  5214  imadiflem  5267  fnop  5291  ssimaex  5547  isosolem  5792  acexmidlem2  5839  fnovex  5875  cnvoprab  6202  smores3  6261  freccllem  6370  riinerm  6574  pw1fin  6876  enq0sym  7373  peano5nnnn  7833  axcaucvglemres  7840  uzind3  9304  xrltnsym  9729  xsubge0  9817  0fz1  9980  seqf  10396  seq3f1oleml  10438  exp1  10461  expp1  10462  resqrexlemf1  10950  resqrexlemfp1  10951  clim2ser  11278  clim2ser2  11279  isermulc2  11281  summodclem3  11321  fisumss  11333  fsum3cvg3  11337  iserabs  11416  isumshft  11431  isumsplit  11432  geoisum1  11460  geoisum1c  11461  cvgratnnlemnexp  11465  cvgratz  11473  mertenslem2  11477  clim2prod  11480  clim2divap  11481  fprodseq  11524  prodssdc  11530  fprodssdc  11531  effsumlt  11633  efgt1p  11637  gcd0id  11912  lcmgcd  12010  lcmdvds  12011  lcmid  12012  isprm2lem  12048  pcmpt  12273  ennnfonelemjn  12335  neipsm  12794  xmetpsmet  13009  comet  13139  metrest  13146  expcncf  13232  lgscllem  13548  lgsdir2  13574  lgsdirnn0  13588  lgsdinn0  13589  exmid1stab  13880  cvgcmp2nlemabs  13911  nconstwlpolem  13943