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  5268  funeu2  5624  imadif  5674  fnop  5695  ssimaex  5944  tfindsg2  6700  nn0suc  6729  xpexr2  6746  extmptsuppeq  6948  suppss  6954  suppss2  6958  wfr3g  7040  smores3  7078  tfr3ALT  7126  tz7.48-2  7165  swoso  7400  isinf  7789  frfi  7820  dffi3  7949  marypha1lem  7951  ordtypelem7  8043  cnfcom2lem  8209  r1pw  8319  rankxplim3  8355  dfac5  8561  cofsmo  8701  axcclem  8889  zorn2lem7  8934  wloglei  10148  divval  10274  uzind3  11031  xrltnsym  11438  xaddf  11519  xrsupsslem  11594  xrinfmsslem  11595  0fz1  11821  hashunsng  12572  hashgt0elexb  12580  sumss  13783  fsumss  13784  fsumcvg3  13788  abscvgcvg  13872  isumshft  13890  geoisum1  13928  geoisum1c  13929  mertenslem2  13934  zprod  13984  prodss  13994  fprodss  13995  rpnnen2lem5  14264  gcdcllem3  14468  lcmgcd  14565  lcmdvds  14566  lcmfval  14584  lcmfvalOLD  14588  lcmfcl  14594  dvdslcmf  14597  eulerthlem2  14723  ramcl2lem  14955  ramcl2lemOLD  14956  imasvscafn  15436  mreexexlem4d  15546  cycsubgcl  16836  galactghm  17037  odlem2  17181  odlem2OLD  17197  gexlem2  17226  gexlem2OLD  17229  mulgmhm  17461  mulgghm  17462  gsumval3  17534  gsumpt  17587  dprdfeq0  17648  srglmhm  17761  srgrmhm  17762  ringlghm  17825  ringrghm  17826  lssssr  18169  lbsind  18296  mplmonmul  18681  mplcoe1  18682  mplcoe5  18685  cnsubrg  19021  matplusgcell  19450  elcls  20081  neips  20121  opnnei  20128  ordtbaslem  20196  ptclsg  20622  qtopeu  20723  xmetpsmet  21355  comet  21520  metrest  21531  pcorevlem  22049  dyadmbl  22550  mbfeqalem  22590  i1fadd  22645  itg1addlem2  22647  itg2uba  22693  itgss  22761  dvcnp  22865  quotval  23237  vieta1lem2  23256  aalioulem3  23282  ulmdvlem3  23349  dvradcnv  23368  abelthlem6  23383  abelthlem9  23387  abelth  23388  logtayllem  23596  logtayl  23597  cxpcl  23611  recxpcl  23612  cxpcn3lem  23679  leibpi  23860  musum  24112  dchrelbas3  24158  sumdchr2  24190  lgscllem  24223  lgsdir2  24248  dchrvmasumiflem2  24332  rpvmasum2  24342  padicabv  24460  padicabvf  24461  padicabvcxp  24462  nmooval  26396  hiidge0  26743  hommval  27381  hfmmval  27384  nmcfnlbi  27697  mdslmd1i  27974  mdslmd3i  27977  sumdmdlem2  28064  foresf1o  28132  disjdifprg  28181  suppss2fOLD  28233  cnvoprab  28308  xdivval  28389  esumfsupre  28894  dya2iocnei  29106  eulerpartlemgc  29197  eulerpartlemb  29203  eulerpartlemgh  29213  ballotlemfc0  29327  ballotlemfcc  29328  subfacp1lem5  29909  subfacp1lem6  29910  cvmliftlem10  30019  elmrsubrn  30160  colinearperm1  30828  colinearperm5  30832  endofsegid  30851  segcon2  30871  seglecgr12im  30876  segletr  30880  colinbtwnle  30884  broutsideof2  30888  btwnoutside  30891  outsideoftr  30895  outsidele  30898  opnbnd  30980  poimirlem11  31871  poimirlem12  31872  poimirlem16  31876  poimirlem19  31879  poimirlem26  31886  heibor1lem  32061  heiborlem3  32065  heiborlem10  32072  ablo4pnp  32098  crngm4  32156  lkrpssN  32654  pclvalN  33380  polvalN  33395  lclkrlem2x  35023  hgmaprnlem5N  35396  sdrgacs  35993  cntzsdrg  35994  dvgrat  36525  radcnvrat  36527  cncfiooicclem1  37597  fourierdlem101  37897  etransclem24  37949