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  5428  funeu2  5619  imadif  5669  fnop  5690  ssimaex  5938  suppssOLD  6021  suppss2OLD  6529  tfindsg2  6695  nn0suc  6723  xpexr2  6740  extmptsuppeq  6942  suppss  6948  suppss2  6952  smores3  7042  tz7.48-2  7125  swoso  7360  isinf  7752  frfi  7783  dffi3  7909  marypha1lem  7911  ordtypelem7  7967  cnfcom2lem  8162  cnfcom2lemOLD  8170  r1pw  8280  rankxplim3  8316  dfac5  8526  cofsmo  8666  axcclem  8854  zorn2lem7  8899  wloglei  10106  divval  10230  uzind3  10977  uzind3OLD  10979  xrltnsym  11368  xaddf  11448  xrsupsslem  11523  xrinfmsslem  11524  0fz1  11730  hashunsng  12463  hashgt0elexb  12471  sumss  13558  fsumss  13559  fsumcvg3  13563  abscvgcvg  13645  isumshft  13663  geoisum1  13700  geoisum1c  13701  mertenslem2  13706  zprod  13756  prodss  13766  fprodss  13767  rpnnen2lem5  13964  gcdcllem3  14163  eulerthlem2  14324  ramcl2lem  14539  imasvscafn  14954  mreexexlem4d  15064  cycsubgcl  16354  galactghm  16555  odlem2  16690  gexlem2  16729  mulgmhm  16963  mulgghm  16964  gsumval3OLD  17035  gsumval3  17038  gsumpt  17115  gsumptOLD  17116  dprdfeq0  17189  dprdfeq0OLD  17196  srglmhm  17313  srgrmhm  17314  ringlghm  17377  ringrghm  17378  lssssr  17726  lbsind  17853  mplmonmul  18253  mplcoe1  18254  mplcoe5  18258  mplcoe2OLD  18260  cnsubrg  18605  matplusgcell  19062  elcls  19701  neips  19741  opnnei  19748  ordtbaslem  19816  ptclsg  20242  qtopeu  20343  xmetpsmet  20977  comet  21142  metrest  21153  pcorevlem  21652  dyadmbl  22135  mbfeqalem  22175  i1fadd  22228  itg1addlem2  22230  itg2uba  22276  itgss  22344  dvcnp  22448  quotval  22814  vieta1lem2  22833  aalioulem3  22856  ulmdvlem3  22923  dvradcnv  22942  abelthlem6  22957  abelthlem9  22961  abelth  22962  logtayllem  23166  logtayl  23167  cxpcl  23181  recxpcl  23182  cxpcn3lem  23247  leibpi  23399  musum  23593  dchrelbas3  23639  sumdchr2  23671  lgscllem  23704  lgsdir2  23729  dchrvmasumiflem2  23813  rpvmasum2  23823  padicabv  23941  padicabvf  23942  padicabvcxp  23943  nmooval  25805  hiidge0  26142  hommval  26782  hfmmval  26785  nmcfnlbi  27098  mdslmd1i  27375  mdslmd3i  27378  sumdmdlem2  27465  foresf1o  27531  disjdifprg  27575  suppss2f  27625  cnvoprab  27703  xdivval  27775  esumfsupre  28243  dya2iocnei  28426  eulerpartlemgc  28498  eulerpartlemb  28504  eulerpartlemgh  28514  ballotlemfc0  28628  ballotlemfcc  28629  subfacp1lem5  28825  subfacp1lem6  28826  cvmliftlem10  28936  elmrsubrn  29077  wfr3g  29559  tfr3ALT  29582  colinearperm1  29917  colinearperm5  29921  endofsegid  29940  segcon2  29960  seglecgr12im  29965  segletr  29969  colinbtwnle  29973  broutsideof2  29977  btwnoutside  29980  outsideoftr  29984  outsidele  29987  opnbnd  30348  heibor1lem  30510  heiborlem3  30514  heiborlem10  30521  ablo4pnp  30547  crngm4  30605  sdrgacs  31354  cntzsdrg  31355  dvgrat  31397  radcnvrat  31399  lcmgcd  31417  lcmdvds  31418  cncfiooicclem1  31899  fourierdlem101  32193  etransclem24  32244  lkrpssN  35031  pclvalN  35757  polvalN  35772  lclkrlem2x  37400  hgmaprnlem5N  37773