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  1438  exmid1stab  4326  imainss  5183  xpexr2m  5209  funeu2  5383  imadiflem  5440  fnop  5466  ssimaex  5743  isosolem  6003  acexmidlem2  6055  fnovex  6091  cnvoprab  6443  suppssdc  6473  smores3  6537  freccllem  6646  riinerm  6855  pw1fin  7183  enq0sym  7763  peano5nnnn  8223  axcaucvglemres  8230  uzind3  9709  xrltnsym  10145  xsubge0  10233  0fz1  10399  seqf  10850  seq3f1oleml  10902  exp1  10931  expp1  10932  resqrexlemf1  11718  resqrexlemfp1  11719  clim2ser  12047  clim2ser2  12048  isermulc2  12050  summodclem3  12091  fisumss  12103  fsum3cvg3  12107  iserabs  12186  isumshft  12201  isumsplit  12202  geoisum1  12230  geoisum1c  12231  cvgratnnlemnexp  12235  cvgratz  12243  mertenslem2  12247  clim2prod  12250  clim2divap  12251  fprodseq  12294  prodssdc  12300  fprodssdc  12301  effsumlt  12403  efgt1p  12407  gcd0id  12700  nninfctlemfo  12761  lcmgcd  12800  lcmdvds  12801  lcmid  12802  isprm2lem  12838  pcmpt  13066  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemimin  13193  ballotfilemfrcn0  13217  ennnfonelemjn  13237  issgrpd  13675  mulg1  13882  gfsumval  14102  srglmhm  14236  srgrmhm  14237  ringlghm  14304  ringrghm  14305  neipsm  15145  xmetpsmet  15360  comet  15490  metrest  15497  expcncf  15600  lgscllem  16006  lgsdir2  16032  lgsdirnn0  16046  lgsdinn0  16047  eupth2lem3lem7fi  16595  cvgcmp2nlemabs  16942  nconstwlpolem  16977