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  5245  funeu2  5436  imadif  5486  fnop  5507  ssimaex  5749  suppssOLD  5829  suppss2OLD  6310  tfindsg2  6467  nn0suc  6495  xpexr2  6514  extmptsuppeq  6708  suppss  6714  suppss2  6718  smores3  6806  tz7.48-2  6889  swoso  7124  isinf  7518  frfi  7549  dffi3  7673  marypha1lem  7675  ordtypelem7  7730  cnfcom2lem  7926  cnfcom2lemOLD  7934  r1pw  8044  rankxplim3  8080  dfac5  8290  cofsmo  8430  axcclem  8618  zorn2lem7  8663  wloglei  9864  divval  9988  uzind3  10727  uzind3OLD  10729  xrltnsym  11106  xaddf  11186  xrsupsslem  11261  xrinfmsslem  11262  0fz1  11461  hashunsng  12146  hashgt0elexb  12152  sumss  13193  fsumss  13194  fsumcvg3  13198  abscvgcvg  13274  isumshft  13294  geoisum1  13331  geoisum1c  13332  mertenslem2  13337  rpnnen2lem5  13493  gcdcllem3  13689  eulerthlem2  13849  ramcl2lem  14062  imasvscafn  14467  mreexexlem4d  14577  mndcl  15412  cycsubgcl  15696  galactghm  15897  odlem2  16031  gexlem2  16070  mulgmhm  16304  mulgghm  16305  gsumval3OLD  16371  gsumval3  16374  gsumpt  16441  gsumptOLD  16442  dprdfeq0  16498  dprdfeq0OLD  16505  srglmhm  16620  srgrmhm  16621  rnglghm  16679  rngrghm  16680  lssssr  17008  lbsind  17135  mplmonmul  17517  mplcoe1  17518  mplcoe2  17521  mplcoe2OLD  17522  cnsubrg  17842  elcls  18646  neips  18686  opnnei  18693  ordtbaslem  18761  ptclsg  19157  qtopeu  19258  xmetpsmet  19892  comet  20057  metrest  20068  pcorevlem  20567  dyadmbl  21049  mbfeqalem  21089  i1fadd  21142  itg1addlem2  21144  itg2uba  21190  itgss  21258  dvcnp  21362  quotval  21727  vieta1lem2  21746  aalioulem3  21769  ulmdvlem3  21836  dvradcnv  21855  abelthlem6  21870  abelthlem9  21874  abelth  21875  logtayllem  22073  logtayl  22074  cxpcl  22088  recxpcl  22089  cxpcn3lem  22154  leibpi  22306  musum  22500  dchrelbas3  22546  sumdchr2  22578  lgscllem  22611  lgsdir2  22636  dchrvmasumiflem2  22720  rpvmasum2  22730  padicabv  22848  padicabvf  22849  padicabvcxp  22850  nmooval  24108  hiidge0  24445  hommval  25085  hfmmval  25088  nmcfnlbi  25401  mdslmd1i  25678  mdslmd3i  25681  sumdmdlem2  25768  disjdifprg  25864  suppss2f  25899  cnvoprab  25968  xdivval  26039  esumfsupre  26468  dya2iocnei  26645  eulerpartlemgc  26693  eulerpartlemb  26699  eulerpartlemgh  26709  ballotlemfc0  26823  ballotlemfcc  26824  subfacp1lem5  27020  subfacp1lem6  27021  cvmliftlem10  27131  zprod  27397  prodss  27407  fprodss  27408  wfr3g  27670  tfr3ALT  27693  colinearperm1  28040  colinearperm5  28044  endofsegid  28063  segcon2  28083  seglecgr12im  28088  segletr  28092  colinbtwnle  28096  broutsideof2  28100  btwnoutside  28103  outsideoftr  28107  outsidele  28110  opnbnd  28463  heibor1lem  28651  heiborlem3  28655  heiborlem10  28662  ablo4pnp  28688  crngm4  28746  sdrgacs  29501  cntzsdrg  29502  matplusgcell  30761  lkrpssN  32559  pclvalN  33285  polvalN  33300  lclkrlem2x  34926  hgmaprnlem5N  35299