Theorem sylan2br 479

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

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  syl2anbr  483  imainss  5251  funeu2  5607  imadif  5658  fnop  5679  ssimaex  5930  tfindsg2  6688  nn0suc  6717  xpexr2  6734  extmptsuppeq  6939  suppss  6945  suppss2  6949  wfr3g  7034  smores3  7072  tfr3ALT  7120  tz7.48-2  7159  swoso  7394  isinf  7785  frfi  7816  dffi3  7945  marypha1lem  7947  ordtypelem7  8039  cnfcom2lem  8206  r1pw  8316  rankxplim3  8352  dfac5  8559  cofsmo  8699  axcclem  8887  zorn2lem7  8932  wloglei  10146  divval  10272  uzind3  11029  xrltnsym  11436  xaddf  11517  xrsupsslem  11592  xrinfmsslem  11593  0fz1  11819  hashunsng  12571  hashgt0elexb  12579  sumss  13790  fsumss  13791  fsumcvg3  13795  abscvgcvg  13879  isumshft  13897  geoisum1  13935  geoisum1c  13936  mertenslem2  13941  zprod  13991  prodss  14001  fprodss  14002  rpnnen2lem5  14271  gcdcllem3  14475  lcmgcd  14572  lcmdvds  14573  lcmfval  14591  lcmfvalOLD  14595  lcmfcl  14601  dvdslcmf  14604  eulerthlem2  14730  ramcl2lem  14962  ramcl2lemOLD  14963  imasvscafn  15443  mreexexlem4d  15553  cycsubgcl  16843  galactghm  17044  odlem2  17188  odlem2OLD  17204  gexlem2  17233  gexlem2OLD  17236  mulgmhm  17468  mulgghm  17469  gsumval3  17541  gsumpt  17594  dprdfeq0  17655  srglmhm  17768  srgrmhm  17769  ringlghm  17832  ringrghm  17833  lssssr  18176  lbsind  18303  mplmonmul  18688  mplcoe1  18689  mplcoe5  18692  cnsubrg  19028  matplusgcell  19458  elcls  20089  neips  20129  opnnei  20136  ordtbaslem  20204  ptclsg  20630  qtopeu  20731  xmetpsmet  21363  comet  21528  metrest  21539  pcorevlem  22057  dyadmbl  22558  mbfeqalem  22598  i1fadd  22653  itg1addlem2  22655  itg2uba  22701  itgss  22769  dvcnp  22873  quotval  23245  vieta1lem2  23264  aalioulem3  23290  ulmdvlem3  23357  dvradcnv  23376  abelthlem6  23391  abelthlem9  23395  abelth  23396  logtayllem  23604  logtayl  23605  cxpcl  23619  recxpcl  23620  cxpcn3lem  23687  leibpi  23868  musum  24120  dchrelbas3  24166  sumdchr2  24198  lgscllem  24231  lgsdir2  24256  dchrvmasumiflem2  24340  rpvmasum2  24350  padicabv  24468  padicabvf  24469  padicabvcxp  24470  nmooval  26404  hiidge0  26751  hommval  27389  hfmmval  27392  nmcfnlbi  27705  mdslmd1i  27982  mdslmd3i  27985  sumdmdlem2  28072  foresf1o  28139  disjdifprg  28185  suppss2fOLD  28237  cnvoprab  28308  xdivval  28388  esumfsupre  28892  dya2iocnei  29104  eulerpartlemgc  29195  eulerpartlemb  29201  eulerpartlemgh  29211  ballotlemfc0  29325  ballotlemfcc  29326  subfacp1lem5  29907  subfacp1lem6  29908  cvmliftlem10  30017  elmrsubrn  30158  colinearperm1  30829  colinearperm5  30833  endofsegid  30852  segcon2  30872  seglecgr12im  30877  segletr  30881  colinbtwnle  30885  broutsideof2  30889  btwnoutside  30892  outsideoftr  30896  outsidele  30899  opnbnd  30981  poimirlem11  31951  poimirlem12  31952  poimirlem16  31956  poimirlem19  31959  poimirlem26  31966  heibor1lem  32141  heiborlem3  32145  heiborlem10  32152  ablo4pnp  32178  crngm4  32236  lkrpssN  32729  pclvalN  33455  polvalN  33470  lclkrlem2x  35098  hgmaprnlem5N  35471  sdrgacs  36067  cntzsdrg  36068  dvgrat  36661  radcnvrat  36663  cncfiooicclem1  37771  fourierdlem101  38071  etransclem24  38123