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  2342  bm1.1  2423  eqtr3  2457  morex  3138  psssstr  3457  reuss2  3625  reupick  3629  reximdva0  3643  rabsneu  3945  opabss  4348  triun  4393  poirr  4647  wefrc  4709  xpcan  5269  fnfco  5572  suppssrOLD  5832  eldmrexrnb  5845  fnressn  5889  fvtp3  5922  fvtp3g  5925  f1mpt  5969  offval  6322  ordsucuniel  6430  onzsl  6452  soex  6516  fun11iun  6532  dfoprab3  6625  1stconst  6656  2ndconst  6657  poxp  6679  fnwelem  6682  suppssr  6715  suppsssn  6719  oeordsuc  7025  oelim2  7026  omsmolem  7084  fisucdomOLD  7508  ssnnfi  7524  fiint  7580  unifi  7592  indexfi  7611  iinfi  7659  unwdomg  7791  inf3lem5  7830  rankr1bg  8002  rankr1c  8020  carden2a  8128  dfac8clem  8194  dfac5lem4  8288  pwsdompw  8365  cfsuc  8418  cflim2  8424  enfin2i  8482  isf34lem4  8538  axdc4lem  8616  zornn0g  8666  uniimadomf  8701  fpwwe2lem8  8796  fpwwe2lem12  8800  fpwwe2lem13  8801  pwfseqlem1  8817  pwfseqlem5  8822  intgru  8973  addclpi  9053  addnidpi  9062  ltsonq  9130  nqpr  9175  reclem3pr  9210  recexsr  9266  supsrlem  9270  infmrcl  10301  nnnn0addcl  10602  un0addcl  10605  un0mulcl  10606  nn0nndivcl  10637  nn0ge0div  10703  uzind3  10727  uzind3OLD  10729  uzind4  10904  zsupss  10936  rpnnen1lem1  10971  rpnnen1lem2  10972  rpnnen1lem3  10973  rpnnen1lem5  10975  ltsubrp  11014  ltaddrp  11015  xrlttr  11109  qbtwnxr  11162  xltnegi  11178  xaddnemnf  11196  xaddnepnf  11197  xaddcom  11200  xnegdi  11203  xsubge0  11216  xrub  11266  fzind2  11629  seqof  11855  expp1  11864  expneg  11865  expcllem  11868  mulexpz  11896  expaddz  11900  expmulz  11902  faclbnd4lem3  12063  faclbnd4  12065  brfi1uzind  12211  swrd00  12306  swrd0  12319  cats1un  12362  cshw0  12423  cshwn  12426  shftf  12560  sqrdiv  12747  leabs  12780  mulcn2  13065  summolem2  13185  fsumrev2  13241  geomulcvg  13328  ruclem6  13509  dvdseq  13572  dvdsfac  13580  gcdcllem1  13687  rpexp1i  13799  hashdvds  13842  iserodd  13894  pcqcl  13915  pcid  13931  ismred  14532  funcpropd  14802  natpropd  14878  lubun  15285  odupos  15297  issubmd  15468  grpinvnzcl  15589  mulgneg  15636  mulgnn0z  15638  symgfixf1  15934  symgsssg  15964  symgfisg  15965  pgpssslw  16104  sylow2alem2  16108  sylow2a  16109  oddvdssubg  16328  gsumzunsnd  16441  gsumunsnd  16442  gsum2dlem1  16451  gsum2dlem2  16452  gsum2dOLD  16454  ablfac1eu  16564  pgpfac1lem5  16570  gsumdixpOLD  16690  gsumdixp  16691  dvdsrcl2  16732  isdrngd  16837  evlslem4OLD  17570  evlslem4  17571  coe1tmmul2  17709  cnsubrg  17853  psgnodpm  17998  gsumcom3  18279  intcld  18624  neiptopnei  18716  ordtrest2lem  18787  lmss  18882  cmpcovf  18974  cncmp  18975  fincmp  18976  cmpsublem  18982  cmpsub  18983  uncon  19013  1stcfb  19029  2ndcsep  19043  1stckgenlem  19106  ptbasin  19130  ptbasfi  19134  ptunimpt  19148  ptuniconst  19151  dfac14  19171  ptcnp  19175  xkoptsub  19207  xkococnlem  19212  xkoinjcn  19240  qtopcmplem  19260  qtophmeo  19370  fbfinnfr  19394  isfcls  19562  psmettri2  19865  xmetrtri  19910  xmetrtri2  19911  blssioo  20352  divcn  20424  bndth  20510  resscdrg  20850  minveclem3  20896  finiunmbl  21005  opnmbllem  21061  ismbf2d  21099  itg2seq  21200  ellimc2  21332  limcmpt2  21339  limcres  21341  dvlem  21351  dvidlem  21370  dvrec  21409  dveflem  21431  dvlip  21445  coe1mul3  21551  dvtaylp  21815  leibpilem2  22316  leibpi  22317  wilthlem2  22387  basellem3  22400  dvdsflip  22502  dchreq  22577  dchrsum  22588  lgsval3  22633  lgsdir2lem4  22645  2sqlem6  22688  rpvmasumlem  22716  dchrisum0fno1  22740  rpvmasum2  22741  pntrsumbnd2  22796  ostthlem1  22856  colmid  23059  axcontlem2  23179  axcontlem7  23184  umgraex  23225  usgraidx2vlem1  23277  nbgraf1olem3  23320  nbgraf1olem5  23322  cusconngra  23530  grpoidinvlem3  23661  ablo32  23741  ablomuldiv  23744  ablodivdiv  23745  ablodiv32  23747  nvadd12  23969  nvscom  23977  nvsubsub23  24010  dipassr  24214  htthlem  24287  hsn0elch  24619  shscli  24688  nmopun  25386  branmfn  25477  mdslj1i  25691  mdslj2i  25692  atss  25718  chcv1  25727  dmdbr5ati  25794  fcnvgreu  25959  isoun  25965  gsumunsnf  26213  ordtrest2NEWlem  26321  esumsplit  26475  esumpcvgval  26496  sigaclcu2  26532  volmeas  26616  mbfmco2  26649  oddpwdc  26706  eulerpartlemgvv  26728  ballotlemfc0  26844  ballotlemfcc  26845  subfacp1lem4  27040  erdszelem7  27054  erdszelem8  27055  erdsze2lem2  27061  rescon  27104  cvmsdisj  27128  cvmscld  27131  climuzcnv  27285  prodmolem2  27417  zprod  27419  prodsn  27442  pocnv  27543  trpredmintr  27664  cgrid2  28003  btwncom  28014  btwnswapid2  28018  colinearperm1  28062  colinearperm3  28063  colinearperm2  28064  colinearperm4  28065  lineext  28076  colinbtwnle  28118  broutsideof2  28122  outsideofcom  28128  linecom  28150  linerflx2  28151  lineintmo  28157  bpolydiflem  28166  bpoly2  28169  bpoly3  28170  hfext  28190  fin2solem  28386  opnmbllem0  28398  mblfinlem3  28401  mbfposadd  28410  itg2addnclem3  28416  bddiblnc  28433  ftc1anclem6  28443  ftc1anc  28446  ntruni  28493  clsint2  28495  locfincmp  28547  neibastop1  28551  eqfnun  28586  ac6gf  28597  heibor1lem  28679  isdrngo2  28735  unichnidl  28802  isfldidl  28839  ismrcd1  29005  isnacs3  29017  pellfundglb  29197  jm2.22  29315  jm2.23  29316  isnumbasgrplem1  29428  hbtlem6  29456  rngunsnply  29501  hashgcdlem  29536  phisum  29538  afv0nbfvbi  30028  wwlktovfo  30224  reuccats1  30232  wlkv0  30262  wlknwwlknfun  30313  wlknwwlkninj  30314  wlknwwlknsur  30315  wlkiswwlkfun  30320  wlkiswwlkinj  30321  wlkiswwlksur  30322  wwlkextfun  30332  wwlkextsur  30334  clwwlkf  30427  lspsslco  30902  bnj521  31657  bnj1109  31709  bnj1294  31740  bnj545  31817  bnj605  31829  bnj594  31834  bnj934  31857  bnj953  31861  bnj1137  31915  bnj1174  31923  bnj1388  31953  bj-snsetex  32356  lkrss2N  32707  elpadd0  33346  ltrnu  33658  tendoex  34512  cdlemm10N  34656  dicfnN  34721  dihmeetlem2N  34837  dihlatat  34875  lcfrlem9  35088