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  7799  peano5nnnn  8259  axcaucvglemres  8266  uzind3  9763  xrltnsym  10205  xsubge0  10293  0fz1  10459  seqf  10914  seq3f1oleml  10966  exp1  10995  expp1  10996  resqrexlemf1  11788  resqrexlemfp1  11789  clim2ser  12119  clim2ser2  12120  isermulc2  12122  summodclem3  12163  fisumss  12175  fsum3cvg3  12179  iserabs  12258  isumshft  12273  isumsplit  12274  geoisum1  12302  geoisum1c  12303  cvgratnnlemnexp  12307  cvgratz  12315  mertenslem2  12319  clim2prod  12322  clim2divap  12323  fprodseq  12366  prodssdc  12372  fprodssdc  12373  effsumlt  12475  efgt1p  12479  gcd0id  12772  nninfctlemfo  12833  lcmgcd  12872  lcmdvds  12873  lcmid  12874  isprm2lem  12910  pcmpt  13142  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemimin  13298  ballotfilemfrcn0  13322  ennnfonelemjn  13342  issgrpd  13776  mulg1  13981  gsumvalfi  14201  srglmhm  14346  srgrmhm  14347  ringlghm  14415  ringrghm  14416  neipsm  15304  xmetpsmet  15519  comet  15649  metrest  15656  expcncf  15759  lgscllem  16224  lgsdir2  16250  lgsdirnn0  16264  lgsdinn0  16265  eupth2lem3lem7fi  16813  cvgcmp2nlemabs  17179  nconstwlpolem  17213