Theorem sylan2b 473

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 472	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367

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 369

This theorem is referenced by:  syl2anb  477  bianir  968  eupickb  2311  bm1.1OLD  2386  eqtr3  2430  elnelne1  2751  elnelne2  2752  morex  3233  psssstr  3549  reuss2  3730  reupick  3734  reximdva0  3750  rabsneu  4047  opabss  4456  triun  4502  poirr  4755  wefrc  4817  xpcan  5261  fnfco  5733  suppssrOLD  5999  fnressn  6063  fvtp3  6100  fvtp3g  6103  f1mpt  6150  offval  6528  ordsucuniel  6642  onzsl  6664  soex  6727  fun11iun  6744  dfoprab3  6840  1stconst  6872  2ndconst  6873  poxp  6896  fnwelem  6899  suppssr  6934  suppsssn  6938  oeordsuc  7280  oelim2  7281  omsmolem  7339  ssnnfi  7774  fiint  7831  unifi  7843  indexfi  7862  iinfi  7911  unwdomg  8044  inf3lem5  8082  rankr1bg  8253  rankr1c  8271  carden2a  8379  dfac8clem  8445  dfac5lem4  8539  pwsdompw  8616  cfsuc  8669  cflim2  8675  enfin2i  8733  isf34lem4  8789  axdc4lem  8867  zornn0g  8917  uniimadomf  8952  fpwwe2lem8  9045  fpwwe2lem12  9049  fpwwe2lem13  9050  pwfseqlem1  9066  pwfseqlem5  9071  intgru  9222  addclpi  9300  addnidpi  9309  ltsonq  9377  nqpr  9422  reclem3pr  9457  recexsr  9514  supsrlem  9518  infmrcl  10562  nnnn0addcl  10867  un0addcl  10870  un0mulcl  10871  nn0nndivcl  10904  nn0ge0div  10973  uzind3  10997  uzind4  11185  zsupss  11216  rpnnen1lem1  11253  rpnnen1lem2  11254  rpnnen1lem3  11255  rpnnen1lem5  11257  ltsubrp  11298  ltaddrp  11299  xrlttr  11399  qbtwnxr  11452  xltnegi  11468  xaddnemnf  11486  xaddnepnf  11487  xaddcom  11490  xnegdi  11493  xsubge0  11506  xrub  11556  fzind2  11961  seqof  12208  expp1  12217  expneg  12218  expcllem  12221  mulexpz  12250  expaddz  12254  expmulz  12256  faclbnd4lem3  12417  faclbnd4  12419  brfi1uzind  12581  swrd00  12699  swrd0  12715  cats1un  12757  reuccats1  12762  cshw0  12821  cshwn  12824  wwlktovfo  12952  shftf  13061  sqrtdiv  13248  leabs  13281  mulcn2  13567  summolem2  13687  fsumrev2  13748  geomulcvg  13837  prodmolem2  13894  zprod  13896  prodsn  13919  bpolydiflem  13999  bpoly2  14002  bpoly3  14003  ruclem6  14177  dvdseq  14242  dvdsfac  14250  gcdcllem1  14358  rpexp1i  14471  hashdvds  14514  iserodd  14568  pcqcl  14589  pcid  14605  ismred  15216  funcpropd  15513  natpropd  15589  lubun  16077  odupos  16089  issubmd  16304  grpinvnzcl  16434  mulgneg  16484  mulgnn0z  16486  symgfixf1  16786  symgsssg  16816  symgfisg  16817  pgpssslw  16958  sylow2alem2  16962  sylow2a  16963  oddvdssubg  17185  gsumzunsnd  17303  gsumunsnfd  17304  gsum2dlem1  17318  gsum2dlem2  17319  gsum2dOLD  17321  ablfac1eu  17444  pgpfac1lem5  17450  gsumdixpOLD  17577  gsumdixp  17578  dvdsrcl2  17619  isdrngd  17741  evlslem4OLD  18493  evlslem4  18494  coe1tmmul2  18637  cnsubrg  18798  psgnodpm  18922  gsumcom3  19193  mpt2matmul  19240  cpmidpmat  19666  intcld  19833  neiptopnei  19926  ordtrest2lem  19997  lmss  20092  cmpcovf  20184  cncmp  20185  fincmp  20186  cmpsublem  20192  cmpsub  20193  uncon  20222  1stcfb  20238  2ndcsep  20252  refun0  20308  locfincmp  20319  1stckgenlem  20346  ptbasin  20370  ptbasfi  20374  ptunimpt  20388  ptuniconst  20391  dfac14  20411  ptcnp  20415  xkoptsub  20447  xkococnlem  20452  xkoinjcn  20480  qtopcmplem  20500  qtophmeo  20610  fbfinnfr  20634  isufil2  20701  isfcls  20802  xmetrtri  21150  xmetrtri2  21151  blssioo  21592  divcn  21664  bndth  21750  resscdrg  22090  minveclem3  22136  finiunmbl  22246  opnmbllem  22302  ismbf2d  22340  itg2seq  22441  ellimc2  22573  limcmpt2  22580  limcres  22582  dvlem  22592  dvidlem  22611  dvrec  22650  dveflem  22672  dvlip  22686  coe1mul3  22792  dvtaylp  23057  leibpilem2  23597  leibpi  23598  wilthlem2  23724  basellem3  23737  dvdsflip  23839  dchreq  23914  dchrsum  23925  lgsval3  23970  lgsdir2lem4  23982  2sqlem6  24025  rpvmasumlem  24053  dchrisum0fno1  24077  rpvmasum2  24078  pntrsumbnd2  24133  ostthlem1  24193  colmid  24451  lmiisolem  24552  dfcgra2  24579  axcontlem2  24685  axcontlem7  24690  umgraex  24740  usgraidx2vlem1  24808  nbgraf1olem3  24860  nbgraf1olem5  24862  cusconngra  25093  wlknwwlknfun  25127  wlknwwlkninj  25128  wlknwwlknsur  25129  wlkiswwlkfun  25134  wlkiswwlkinj  25135  wlkiswwlksur  25136  wwlkextfun  25146  wwlkextsur  25148  wlkv0  25177  clwwlkf  25211  grpoidinvlem3  25622  ablo32  25702  ablomuldiv  25705  ablodivdiv  25706  ablodiv32  25708  nvadd12  25930  nvscom  25938  nvsubsub23  25971  dipassr  26175  htthlem  26248  hsn0elch  26580  shscli  26649  nmopun  27346  branmfn  27437  mdslj1i  27651  mdslj2i  27652  atss  27678  chcv1  27687  dmdbr5ati  27754  fcnvgreu  27957  isoun  27964  ordtrest2NEWlem  28357  esumsplit  28500  esumpad2  28503  esumpcvgval  28525  sigaclcu2  28568  ldgenpisyslem1  28611  volmeas  28680  mbfmco2  28713  omsmeas  28771  oddpwdc  28799  eulerpartlemgvv  28821  ballotlemfc0  28937  ballotlemfcc  28938  bnj521  29119  bnj1109  29172  bnj1294  29203  bnj545  29280  bnj605  29292  bnj594  29297  bnj934  29320  bnj953  29324  bnj1137  29378  bnj1174  29386  bnj1388  29416  subfacp1lem4  29480  erdszelem7  29494  erdszelem8  29495  erdsze2lem2  29501  rescon  29543  cvmsdisj  29567  cvmscld  29570  mclsax  29781  climuzcnv  29889  pocnv  29977  trpredmintr  30045  cgrid2  30341  btwncom  30352  btwnswapid2  30356  colinearperm1  30400  colinearperm3  30401  colinearperm2  30402  colinearperm4  30403  lineext  30414  colinbtwnle  30456  broutsideof2  30460  outsideofcom  30466  linecom  30488  linerflx2  30489  lineintmo  30495  fwddifn0  30502  hfext  30521  ntruni  30555  clsint2  30557  neibastop1  30587  bj-snsetex  31086  relowlssretop  31280  fin2solem  31411  opnmbllem0  31422  mblfinlem3  31425  mbfposadd  31434  itg2addnclem3  31441  bddiblnc  31458  ftc1anclem6  31468  ftc1anc  31471  eqfnun  31494  ac6gf  31505  heibor1lem  31587  isdrngo2  31643  unichnidl  31710  isfldidl  31747  cnf1dd  31772  lkrss2N  32187  elpadd0  32826  ltrnu  33138  tendoex  33994  cdlemm10N  34138  dicfnN  34203  dihmeetlem2N  34319  dihlatat  34357  lcfrlem9  34570  ismrcd1  34992  isnacs3  35004  pellfundglb  35182  jm2.22  35299  jm2.23  35300  isnumbasgrplem1  35414  hbtlem6  35442  rngunsnply  35486  hashgcdlem  35521  phisum  35523  dvgrat  36041  cvgdvgrat  36042  lcmgcdlem  36060  nznngen  36069  uzmptshftfval  36099  iccshift  36926  iooshift  36930  prodsnf  36955  itgperiod  37148  fourierdlem42  37299  fourierdlem68  37325  fourierdlem93  37350  elprneb  37663  usgedgppr  38027  usgpredgv  38028  usgpredgvALT  38029  edgssv2ALT  38030  edgssv2  38031  usgedgvadf1lem1  38042  usgedgvadf1ALTlem1  38045  rabsubmgmd  38108  2zlidl  38251  lspsslco  38549