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  6569  freccllem  6678  riinerm  6887  pw1fin  7223  enq0sym  7805  peano5nnnn  8265  axcaucvglemres  8272  uzind3  9769  xrltnsym  10211  xsubge0  10299  0fz1  10465  seqf  10921  seq3f1oleml  10973  exp1  11002  expp1  11003  resqrexlemf1  11795  resqrexlemfp1  11796  clim2ser  12127  clim2ser2  12128  isermulc2  12130  summodclem3  12171  fisumss  12183  fsum3cvg3  12187  iserabs  12266  isumshft  12281  isumsplit  12282  geoisum1  12310  geoisum1c  12311  cvgratnnlemnexp  12315  cvgratz  12323  mertenslem2  12327  clim2prod  12330  clim2divap  12331  fprodseq  12374  prodssdc  12380  fprodssdc  12381  effsumlt  12483  efgt1p  12487  gcd0id  12780  nninfctlemfo  12841  lcmgcd  12880  lcmdvds  12881  lcmid  12882  isprm2lem  12918  pcmpt  13150  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemimin  13306  ballotfilemfrcn0  13330  ennnfonelemjn  13350  issgrpd  13785  mulg1  13990  gsumvalfi  14241  srglmhm  14403  srgrmhm  14404  ringlghm  14472  ringrghm  14473  neipsm  15397  xmetpsmet  15612  comet  15742  metrest  15749  expcncf  15852  lgscllem  16348  lgsdir2  16374  lgsdirnn0  16388  lgsdinn0  16389  eupth2lem3lem7fi  16937  cvgcmp2nlemabs  17304  nconstwlpolem  17339