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  5412  funeu2  5604  imadif  5654  fnop  5675  ssimaex  5923  suppssOLD  6005  suppss2OLD  6505  tfindsg2  6667  nn0suc  6695  xpexr2  6715  extmptsuppeq  6914  suppss  6920  suppss2  6924  smores3  7014  tz7.48-2  7097  swoso  7332  isinf  7723  frfi  7754  dffi3  7880  marypha1lem  7882  ordtypelem7  7938  cnfcom2lem  8134  cnfcom2lemOLD  8142  r1pw  8252  rankxplim3  8288  dfac5  8498  cofsmo  8638  axcclem  8826  zorn2lem7  8871  wloglei  10074  divval  10198  uzind3  10943  uzind3OLD  10945  xrltnsym  11332  xaddf  11412  xrsupsslem  11487  xrinfmsslem  11488  0fz1  11694  hashunsng  12414  hashgt0elexb  12420  sumss  13495  fsumss  13496  fsumcvg3  13500  abscvgcvg  13582  isumshft  13603  geoisum1  13640  geoisum1c  13641  mertenslem2  13646  rpnnen2lem5  13802  gcdcllem3  13999  eulerthlem2  14160  ramcl2lem  14375  imasvscafn  14781  mreexexlem4d  14891  mndcl  15726  cycsubgcl  16015  galactghm  16216  odlem2  16352  gexlem2  16391  mulgmhm  16625  mulgghm  16626  gsumval3OLD  16692  gsumval3  16695  gsumpt  16772  gsumptOLD  16773  dprdfeq0  16845  dprdfeq0OLD  16852  srglmhm  16967  srgrmhm  16968  rnglghm  17027  rngrghm  17028  lssssr  17375  lbsind  17502  mplmonmul  17890  mplcoe1  17891  mplcoe5  17895  mplcoe2OLD  17897  cnsubrg  18239  matplusgcell  18695  elcls  19333  neips  19373  opnnei  19380  ordtbaslem  19448  ptclsg  19844  qtopeu  19945  xmetpsmet  20579  comet  20744  metrest  20755  pcorevlem  21254  dyadmbl  21737  mbfeqalem  21777  i1fadd  21830  itg1addlem2  21832  itg2uba  21878  itgss  21946  dvcnp  22050  quotval  22415  vieta1lem2  22434  aalioulem3  22457  ulmdvlem3  22524  dvradcnv  22543  abelthlem6  22558  abelthlem9  22562  abelth  22563  logtayllem  22761  logtayl  22762  cxpcl  22776  recxpcl  22777  cxpcn3lem  22842  leibpi  22994  musum  23188  dchrelbas3  23234  sumdchr2  23266  lgscllem  23299  lgsdir2  23324  dchrvmasumiflem2  23408  rpvmasum2  23418  padicabv  23536  padicabvf  23537  padicabvcxp  23538  nmooval  25340  hiidge0  25677  hommval  26317  hfmmval  26320  nmcfnlbi  26633  mdslmd1i  26910  mdslmd3i  26913  sumdmdlem2  27000  disjdifprg  27095  suppss2f  27136  cnvoprab  27204  xdivval  27269  esumfsupre  27703  dya2iocnei  27879  eulerpartlemgc  27927  eulerpartlemb  27933  eulerpartlemgh  27943  ballotlemfc0  28057  ballotlemfcc  28058  subfacp1lem5  28254  subfacp1lem6  28255  cvmliftlem10  28365  zprod  28632  prodss  28642  fprodss  28643  wfr3g  28905  tfr3ALT  28928  colinearperm1  29275  colinearperm5  29279  endofsegid  29298  segcon2  29318  seglecgr12im  29323  segletr  29327  colinbtwnle  29331  broutsideof2  29335  btwnoutside  29338  outsideoftr  29342  outsidele  29345  opnbnd  29707  heibor1lem  29895  heiborlem3  29899  heiborlem10  29906  ablo4pnp  29932  crngm4  29990  sdrgacs  30744  cntzsdrg  30745  lkrpssN  33835  pclvalN  34561  polvalN  34576  lclkrlem2x  36202  hgmaprnlem5N  36575