Theorem sylan2b 475

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2b.1	|- ( ph <-> ch )
sylan2b.2	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylan2b	|- ( ( ps /\ ph ) -> th )

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan2b.1	. . 3 |- ( ph <-> ch )
2	1	biimpi 194	. 2 |- ( ph -> ch )
3		sylan2b.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:  syl2anb  479  bianir  958  eupickb  2351  bm1.1OLD  2435  eqtr3  2479  morex  3240  psssstr  3560  reuss2  3728  reupick  3732  reximdva0  3746  rabsneu  4048  opabss  4451  triun  4496  poirr  4750  wefrc  4812  xpcan  5372  fnfco  5675  suppssrOLD  5936  eldmrexrnb  5949  fnressn  5993  fvtp3  6026  fvtp3g  6029  f1mpt  6073  offval  6427  ordsucuniel  6535  onzsl  6557  soex  6621  fun11iun  6637  dfoprab3  6730  1stconst  6761  2ndconst  6762  poxp  6784  fnwelem  6787  suppssr  6820  suppsssn  6824  oeordsuc  7133  oelim2  7134  omsmolem  7192  fisucdomOLD  7617  ssnnfi  7633  fiint  7689  unifi  7701  indexfi  7720  iinfi  7768  unwdomg  7900  inf3lem5  7939  rankr1bg  8111  rankr1c  8129  carden2a  8237  dfac8clem  8303  dfac5lem4  8397  pwsdompw  8474  cfsuc  8527  cflim2  8533  enfin2i  8591  isf34lem4  8647  axdc4lem  8725  zornn0g  8775  uniimadomf  8810  fpwwe2lem8  8905  fpwwe2lem12  8909  fpwwe2lem13  8910  pwfseqlem1  8926  pwfseqlem5  8931  intgru  9082  addclpi  9162  addnidpi  9171  ltsonq  9239  nqpr  9284  reclem3pr  9319  recexsr  9375  supsrlem  9379  infmrcl  10410  nnnn0addcl  10711  un0addcl  10714  un0mulcl  10715  nn0nndivcl  10746  nn0ge0div  10812  uzind3  10836  uzind3OLD  10838  uzind4  11013  zsupss  11045  rpnnen1lem1  11080  rpnnen1lem2  11081  rpnnen1lem3  11082  rpnnen1lem5  11084  ltsubrp  11123  ltaddrp  11124  xrlttr  11218  qbtwnxr  11271  xltnegi  11287  xaddnemnf  11305  xaddnepnf  11306  xaddcom  11309  xnegdi  11312  xsubge0  11325  xrub  11375  fzind2  11738  seqof  11964  expp1  11973  expneg  11974  expcllem  11977  mulexpz  12005  expaddz  12009  expmulz  12011  faclbnd4lem3  12172  faclbnd4  12174  brfi1uzind  12321  swrd00  12416  swrd0  12429  cats1un  12472  cshw0  12533  cshwn  12536  shftf  12670  sqrdiv  12857  leabs  12890  mulcn2  13175  summolem2  13295  fsumrev2  13351  geomulcvg  13438  ruclem6  13619  dvdseq  13682  dvdsfac  13690  gcdcllem1  13797  rpexp1i  13909  hashdvds  13952  iserodd  14004  pcqcl  14025  pcid  14041  ismred  14642  funcpropd  14912  natpropd  14988  lubun  15395  odupos  15407  issubmd  15579  grpinvnzcl  15700  mulgneg  15747  mulgnn0z  15749  symgfixf1  16045  symgsssg  16075  symgfisg  16076  pgpssslw  16217  sylow2alem2  16221  sylow2a  16222  oddvdssubg  16441  gsumzunsnd  16556  gsumunsnd  16557  gsum2dlem1  16566  gsum2dlem2  16567  gsum2dOLD  16569  ablfac1eu  16679  pgpfac1lem5  16685  gsumdixpOLD  16806  gsumdixp  16807  dvdsrcl2  16848  isdrngd  16963  evlslem4OLD  17697  evlslem4  17698  coe1tmmul2  17837  cnsubrg  17982  psgnodpm  18127  gsumcom3  18408  intcld  18760  neiptopnei  18852  ordtrest2lem  18923  lmss  19018  cmpcovf  19110  cncmp  19111  fincmp  19112  cmpsublem  19118  cmpsub  19119  uncon  19149  1stcfb  19165  2ndcsep  19179  1stckgenlem  19242  ptbasin  19266  ptbasfi  19270  ptunimpt  19284  ptuniconst  19287  dfac14  19307  ptcnp  19311  xkoptsub  19343  xkococnlem  19348  xkoinjcn  19376  qtopcmplem  19396  qtophmeo  19506  fbfinnfr  19530  isfcls  19698  psmettri2  20001  xmetrtri  20046  xmetrtri2  20047  blssioo  20488  divcn  20560  bndth  20646  resscdrg  20986  minveclem3  21032  finiunmbl  21141  opnmbllem  21197  ismbf2d  21235  itg2seq  21336  ellimc2  21468  limcmpt2  21475  limcres  21477  dvlem  21487  dvidlem  21506  dvrec  21545  dveflem  21567  dvlip  21581  coe1mul3  21687  dvtaylp  21951  leibpilem2  22452  leibpi  22453  wilthlem2  22523  basellem3  22536  dvdsflip  22638  dchreq  22713  dchrsum  22724  lgsval3  22769  lgsdir2lem4  22781  2sqlem6  22824  rpvmasumlem  22852  dchrisum0fno1  22876  rpvmasum2  22877  pntrsumbnd2  22932  ostthlem1  22992  colmid  23208  axcontlem2  23346  axcontlem7  23351  umgraex  23392  usgraidx2vlem1  23444  nbgraf1olem3  23487  nbgraf1olem5  23489  cusconngra  23697  grpoidinvlem3  23828  ablo32  23908  ablomuldiv  23911  ablodivdiv  23912  ablodiv32  23914  nvadd12  24136  nvscom  24144  nvsubsub23  24177  dipassr  24381  htthlem  24454  hsn0elch  24786  shscli  24855  nmopun  25553  branmfn  25644  mdslj1i  25858  mdslj2i  25859  atss  25885  chcv1  25894  dmdbr5ati  25961  fcnvgreu  26125  isoun  26131  gsumunsnf  26379  ordtrest2NEWlem  26486  esumsplit  26640  esumpcvgval  26661  sigaclcu2  26697  volmeas  26781  mbfmco2  26814  oddpwdc  26871  eulerpartlemgvv  26893  ballotlemfc0  27009  ballotlemfcc  27010  subfacp1lem4  27205  erdszelem7  27219  erdszelem8  27220  erdsze2lem2  27226  rescon  27269  cvmsdisj  27293  cvmscld  27296  climuzcnv  27450  prodmolem2  27582  zprod  27584  prodsn  27607  pocnv  27708  trpredmintr  27829  cgrid2  28168  btwncom  28179  btwnswapid2  28183  colinearperm1  28227  colinearperm3  28228  colinearperm2  28229  colinearperm4  28230  lineext  28241  colinbtwnle  28283  broutsideof2  28287  outsideofcom  28293  linecom  28315  linerflx2  28316  lineintmo  28322  bpolydiflem  28331  bpoly2  28334  bpoly3  28335  hfext  28355  fin2solem  28553  opnmbllem0  28565  mblfinlem3  28568  mbfposadd  28577  itg2addnclem3  28583  bddiblnc  28600  ftc1anclem6  28610  ftc1anc  28613  ntruni  28660  clsint2  28662  locfincmp  28714  neibastop1  28718  eqfnun  28753  ac6gf  28764  heibor1lem  28846  isdrngo2  28902  unichnidl  28969  isfldidl  29006  ismrcd1  29172  isnacs3  29184  pellfundglb  29364  jm2.22  29482  jm2.23  29483  isnumbasgrplem1  29595  hbtlem6  29623  rngunsnply  29668  hashgcdlem  29703  phisum  29705  afv0nbfvbi  30195  wwlktovfo  30391  reuccats1  30399  wlkv0  30429  wlknwwlknfun  30480  wlknwwlkninj  30481  wlknwwlknsur  30482  wlkiswwlkfun  30487  wlkiswwlkinj  30488  wlkiswwlksur  30489  wwlkextfun  30499  wwlkextsur  30501  clwwlkf  30594  lspsslco  31078  cpmidpmat  31327  bnj521  32028  bnj1109  32080  bnj1294  32111  bnj545  32188  bnj605  32200  bnj594  32205  bnj934  32228  bnj953  32232  bnj1137  32286  bnj1174  32294  bnj1388  32324  bj-snsetex  32756  lkrss2N  33120  elpadd0  33759  ltrnu  34071  tendoex  34925  cdlemm10N  35069  dicfnN  35134  dihmeetlem2N  35250  dihlatat  35288  lcfrlem9  35501