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  1442  exmid1stab  4340  imainss  5198  xpexr2m  5224  funeu2  5398  imadiflem  5455  fnop  5481  ssimaex  5758  isosolem  6020  acexmidlem2  6072  fnovex  6108  cnvoprab  6460  suppssdc  6490  smores3  6554  freccllem  6663  riinerm  6872  pw1fin  7207  enq0sym  7789  peano5nnnn  8249  axcaucvglemres  8256  uzind3  9738  xrltnsym  10174  xsubge0  10262  0fz1  10428  seqf  10879  seq3f1oleml  10931  exp1  10960  expp1  10961  resqrexlemf1  11752  resqrexlemfp1  11753  clim2ser  12081  clim2ser2  12082  isermulc2  12084  summodclem3  12125  fisumss  12137  fsum3cvg3  12141  iserabs  12220  isumshft  12235  isumsplit  12236  geoisum1  12264  geoisum1c  12265  cvgratnnlemnexp  12269  cvgratz  12277  mertenslem2  12281  clim2prod  12284  clim2divap  12285  fprodseq  12328  prodssdc  12334  fprodssdc  12335  effsumlt  12437  efgt1p  12441  gcd0id  12734  nninfctlemfo  12795  lcmgcd  12834  lcmdvds  12835  lcmid  12836  isprm2lem  12872  pcmpt  13100  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemimin  13227  ballotfilemfrcn0  13251  ennnfonelemjn  13271  issgrpd  13704  mulg1  13909  gsumvalfi  14129  srglmhm  14271  srgrmhm  14272  ringlghm  14339  ringrghm  14340  neipsm  15178  xmetpsmet  15393  comet  15523  metrest  15530  expcncf  15633  lgscllem  16040  lgsdir2  16066  lgsdirnn0  16080  lgsdinn0  16081  eupth2lem3lem7fi  16629  cvgcmp2nlemabs  16986  nconstwlpolem  17020