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  4208  imainss  5044  xpexr2m  5070  funeu2  5242  imadiflem  5295  fnop  5319  ssimaex  5577  isosolem  5824  acexmidlem2  5871  fnovex  5907  cnvoprab  6234  smores3  6293  freccllem  6402  riinerm  6607  pw1fin  6909  enq0sym  7430  peano5nnnn  7890  axcaucvglemres  7897  uzind3  9365  xrltnsym  9792  xsubge0  9880  0fz1  10044  seqf  10460  seq3f1oleml  10502  exp1  10525  expp1  10526  resqrexlemf1  11016  resqrexlemfp1  11017  clim2ser  11344  clim2ser2  11345  isermulc2  11347  summodclem3  11387  fisumss  11399  fsum3cvg3  11403  iserabs  11482  isumshft  11497  isumsplit  11498  geoisum1  11526  geoisum1c  11527  cvgratnnlemnexp  11531  cvgratz  11539  mertenslem2  11543  clim2prod  11546  clim2divap  11547  fprodseq  11590  prodssdc  11596  fprodssdc  11597  effsumlt  11699  efgt1p  11703  gcd0id  11979  lcmgcd  12077  lcmdvds  12078  lcmid  12079  isprm2lem  12115  pcmpt  12340  ennnfonelemjn  12402  mulg1  12989  srglmhm  13174  srgrmhm  13175  neipsm  13624  xmetpsmet  13839  comet  13969  metrest  13976  expcncf  14062  lgscllem  14378  lgsdir2  14404  lgsdirnn0  14418  lgsdinn0  14419  cvgcmp2nlemabs  14750  nconstwlpolem  14782