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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl2anbr  292  xordc1  1442  exmid1stab  4345  imainss  5203  xpexr2m  5229  funeu2  5403  imadiflem  5460  fnop  5486  ssimaex  5764  isosolem  6030  acexmidlem2  6082  fnovex  6118  cnvoprab  6470  suppssdc  6500  smores3  6564  freccllem  6673  riinerm  6882  pw1fin  7217  enq0sym  7800  peano5nnnn  8260  axcaucvglemres  8267  uzind3  9764  xrltnsym  10206  xsubge0  10294  0fz1  10460  seqf  10916  seq3f1oleml  10968  exp1  10997  expp1  10998  resqrexlemf1  11790  resqrexlemfp1  11791  clim2ser  12122  clim2ser2  12123  isermulc2  12125  summodclem3  12166  fisumss  12178  fsum3cvg3  12182  iserabs  12261  isumshft  12276  isumsplit  12277  geoisum1  12305  geoisum1c  12306  cvgratnnlemnexp  12310  cvgratz  12318  mertenslem2  12322  clim2prod  12325  clim2divap  12326  fprodseq  12369  prodssdc  12375  fprodssdc  12376  effsumlt  12478  efgt1p  12482  gcd0id  12775  nninfctlemfo  12836  lcmgcd  12875  lcmdvds  12876  lcmid  12877  isprm2lem  12913  pcmpt  13145  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemimin  13301  ballotfilemfrcn0  13325  ennnfonelemjn  13345  issgrpd  13780  mulg1  13985  gsumvalfi  14236  srglmhm  14381  srgrmhm  14382  ringlghm  14450  ringrghm  14451  neipsm  15346  xmetpsmet  15561  comet  15691  metrest  15698  expcncf  15801  lgscllem  16292  lgsdir2  16318  lgsdirnn0  16332  lgsdinn0  16333  eupth2lem3lem7fi  16881  cvgcmp2nlemabs  17247  nconstwlpolem  17282