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  4347  imainss  5206  xpexr2m  5232  funeu2  5406  imadiflem  5463  fnop  5489  ssimaex  5767  isosolem  6033  acexmidlem2  6085  fnovex  6121  cnvoprab  6474  suppssdc  6504  smores3  6568  freccllem  6677  riinerm  6886  pw1fin  7221  enq0sym  7805  peano5nnnn  8265  axcaucvglemres  8272  uzind3  9770  xrltnsym  10212  xsubge0  10300  0fz1  10466  seqf  10922  seq3f1oleml  10974  exp1  11003  expp1  11004  resqrexlemf1  11796  resqrexlemfp1  11797  clim2ser  12128  clim2ser2  12129  isermulc2  12131  summodclem3  12172  fisumss  12184  fsum3cvg3  12188  iserabs  12267  isumshft  12282  isumsplit  12283  geoisum1  12311  geoisum1c  12312  cvgratnnlemnexp  12316  cvgratz  12324  mertenslem2  12328  clim2prod  12331  clim2divap  12332  fprodseq  12375  prodssdc  12381  fprodssdc  12382  effsumlt  12484  efgt1p  12488  gcd0id  12781  nninfctlemfo  12842  lcmgcd  12881  lcmdvds  12882  lcmid  12883  isprm2lem  12919  pcmpt  13151  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemimin  13307  ballotfilemfrcn0  13331  ennnfonelemjn  13351  issgrpd  13786  mulg1  13991  gsumvalfi  14242  srglmhm  14404  srgrmhm  14405  ringlghm  14473  ringrghm  14474  neipsm  15380  xmetpsmet  15595  comet  15725  metrest  15732  expcncf  15835  lgscllem  16331  lgsdir2  16357  lgsdirnn0  16371  lgsdinn0  16372  eupth2lem3lem7fi  16920  cvgcmp2nlemabs  17287  nconstwlpolem  17322