Theorem sylan2br 476

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 206	. 2 |- ( ph -> ch )
3		sylan2br.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 474	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  syl2anbr  480  imainss  5255  funeu2  5446  imadif  5496  fnop  5517  ssimaex  5759  suppssOLD  5839  suppss2OLD  6318  tfindsg2  6475  nn0suc  6503  xpexr2  6522  extmptsuppeq  6716  suppss  6722  suppss2  6726  smores3  6817  tz7.48-2  6900  swoso  7135  isinf  7529  frfi  7560  dffi3  7684  marypha1lem  7686  ordtypelem7  7741  cnfcom2lem  7937  cnfcom2lemOLD  7945  r1pw  8055  rankxplim3  8091  dfac5  8301  cofsmo  8441  axcclem  8629  zorn2lem7  8674  wloglei  9875  divval  9999  uzind3  10738  uzind3OLD  10740  xrltnsym  11117  xaddf  11197  xrsupsslem  11272  xrinfmsslem  11273  0fz1  11472  hashunsng  12157  hashgt0elexb  12163  sumss  13204  fsumss  13205  fsumcvg3  13209  abscvgcvg  13285  isumshft  13305  geoisum1  13342  geoisum1c  13343  mertenslem2  13348  rpnnen2lem5  13504  gcdcllem3  13700  eulerthlem2  13860  ramcl2lem  14073  imasvscafn  14478  mreexexlem4d  14588  mndcl  15423  cycsubgcl  15710  galactghm  15911  odlem2  16045  gexlem2  16084  mulgmhm  16318  mulgghm  16319  gsumval3OLD  16385  gsumval3  16388  gsumpt  16457  gsumptOLD  16458  dprdfeq0  16515  dprdfeq0OLD  16522  srglmhm  16637  srgrmhm  16638  rnglghm  16696  rngrghm  16697  lssssr  17037  lbsind  17164  mplmonmul  17546  mplcoe1  17547  mplcoe5  17551  mplcoe2OLD  17553  cnsubrg  17876  elcls  18680  neips  18720  opnnei  18727  ordtbaslem  18795  ptclsg  19191  qtopeu  19292  xmetpsmet  19926  comet  20091  metrest  20102  pcorevlem  20601  dyadmbl  21083  mbfeqalem  21123  i1fadd  21176  itg1addlem2  21178  itg2uba  21224  itgss  21292  dvcnp  21396  quotval  21761  vieta1lem2  21780  aalioulem3  21803  ulmdvlem3  21870  dvradcnv  21889  abelthlem6  21904  abelthlem9  21908  abelth  21909  logtayllem  22107  logtayl  22108  cxpcl  22122  recxpcl  22123  cxpcn3lem  22188  leibpi  22340  musum  22534  dchrelbas3  22580  sumdchr2  22612  lgscllem  22645  lgsdir2  22670  dchrvmasumiflem2  22754  rpvmasum2  22764  padicabv  22882  padicabvf  22883  padicabvcxp  22884  nmooval  24166  hiidge0  24503  hommval  25143  hfmmval  25146  nmcfnlbi  25459  mdslmd1i  25736  mdslmd3i  25739  sumdmdlem2  25826  disjdifprg  25922  suppss2f  25957  cnvoprab  26026  xdivval  26097  esumfsupre  26523  dya2iocnei  26700  eulerpartlemgc  26748  eulerpartlemb  26754  eulerpartlemgh  26764  ballotlemfc0  26878  ballotlemfcc  26879  subfacp1lem5  27075  subfacp1lem6  27076  cvmliftlem10  27186  zprod  27453  prodss  27463  fprodss  27464  wfr3g  27726  tfr3ALT  27749  colinearperm1  28096  colinearperm5  28100  endofsegid  28119  segcon2  28139  seglecgr12im  28144  segletr  28148  colinbtwnle  28152  broutsideof2  28156  btwnoutside  28159  outsideoftr  28163  outsidele  28166  opnbnd  28523  heibor1lem  28711  heiborlem3  28715  heiborlem10  28722  ablo4pnp  28748  crngm4  28806  sdrgacs  29561  cntzsdrg  29562  matplusgcell  30862  lkrpssN  32811  pclvalN  33537  polvalN  33552  lclkrlem2x  35178  hgmaprnlem5N  35551