Theorem sylan2br 493

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  syl2anbr  497  pm2.61danel  2911  imainss  5548  funeu2  5914  imadif  5973  fnop  5994  ssimaex  6263  tfindsg2  7061  nn0suc  7090  xpexr2  7107  extmptsuppeq  7319  suppss  7325  suppss2  7329  wfr3g  7413  smores3  7450  tfr3ALT  7498  tz7.48-2  7537  swoso  7775  isinf  8173  frfi  8205  dffi3  8337  marypha1lem  8339  ordtypelem7  8429  cnfcom2lem  8598  r1pw  8708  rankxplim3  8744  dfac5  8951  cofsmo  9091  axcclem  9279  zorn2lem7  9324  wloglei  10560  divval  10687  uzind3  11471  xrltnsym  11970  xaddf  12055  xrsupsslem  12137  xrinfmsslem  12138  0fz1  12361  hashunsng  13181  hashgt0elexb  13190  sumss  14455  fsumss  14456  fsumcvg3  14460  abscvgcvg  14551  isumshft  14571  geoisum1  14610  geoisum1c  14611  mertenslem2  14617  zprod  14667  prodss  14677  fprodss  14678  rpnnen2lem5  14947  gcdcllem3  15223  lcmgcd  15320  lcmdvds  15321  lcmfval  15334  lcmfcl  15341  dvdslcmf  15344  isprm2lem  15394  eulerthlem2  15487  ramcl2lem  15713  imasvscafn  16197  mreexexlem4d  16307  cycsubgcl  17620  galactghm  17823  odlem2  17958  gexlem2  17997  mulgmhm  18233  mulgghm  18234  gsumval3  18308  gsumpt  18361  dprdfeq0  18421  srglmhm  18535  srgrmhm  18536  ringlghm  18604  ringrghm  18605  lssssr  18953  lbsind  19080  mplmonmul  19464  mplcoe1  19465  mplcoe5  19468  cnsubrg  19806  matplusgcell  20239  elcls  20877  neips  20917  opnnei  20924  ordtbaslem  20992  ptclsg  21418  qtopeu  21519  xmetpsmet  22153  comet  22318  metrest  22329  pcorevlem  22826  dyadmbl  23368  mbfeqalem  23409  i1fadd  23462  itg1addlem2  23464  itg2uba  23510  itgss  23578  dvcnp  23682  quotval  24047  vieta1lem2  24066  aalioulem3  24089  ulmdvlem3  24156  dvradcnv  24175  abelthlem6  24190  abelthlem9  24194  abelth  24195  logtayllem  24405  logtayl  24406  cxpcl  24420  recxpcl  24421  cxpcn3lem  24488  leibpi  24669  musum  24917  dchrelbas3  24963  sumdchr2  24995  lgscllem  25029  lgsdir2  25055  dchrvmasumiflem2  25191  rpvmasum2  25201  padicabv  25319  padicabvf  25320  padicabvcxp  25321  1wlkdlem4  27000  nmooval  27618  hiidge0  27955  hommval  28595  hfmmval  28598  nmcfnlbi  28911  mdslmd1i  29188  mdslmd3i  29191  sumdmdlem2  29278  foresf1o  29343  disjdifprg  29388  cnvoprab  29498  xdivval  29627  esumfsupre  30133  dya2iocnei  30344  eulerpartlemgc  30424  eulerpartlemb  30430  eulerpartlemgh  30440  ballotlemfc0  30554  ballotlemfcc  30555  subfacp1lem5  31166  subfacp1lem6  31167  cvmliftlem10  31276  elmrsubrn  31417  colinearperm1  32169  colinearperm5  32173  endofsegid  32192  segcon2  32212  seglecgr12im  32217  segletr  32221  colinbtwnle  32225  broutsideof2  32229  btwnoutside  32232  outsideoftr  32236  outsidele  32239  opnbnd  32320  matunitlindf  33407  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem19  33428  poimirlem26  33435  heibor1lem  33608  heiborlem3  33612  heiborlem10  33619  ablo4pnp  33679  crngm4  33802  lkrpssN  34450  pclvalN  35176  polvalN  35191  lclkrlem2x  36819  hgmaprnlem5N  37192  sdrgacs  37771  cntzsdrg  37772  dvgrat  38511  radcnvrat  38513  cncfiooicclem1  40106  fourierdlem101  40424  etransclem24  40475  ioorrnopn  40525