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  960  eupickb  2359  bm1.1OLD  2444  eqtr3  2488  morex  3280  psssstr  3603  reuss2  3771  reupick  3775  reximdva0  3789  rabsneu  4095  opabss  4501  triun  4546  poirr  4804  wefrc  4866  xpcan  5434  fnfco  5741  suppssrOLD  6006  eldmrexrnb  6019  fnressn  6064  fvtp3  6101  fvtp3g  6104  f1mpt  6148  offval  6522  ordsucuniel  6630  onzsl  6652  soex  6717  fun11iun  6734  dfoprab3  6830  1stconst  6861  2ndconst  6862  poxp  6885  fnwelem  6888  suppssr  6921  suppsssn  6925  oeordsuc  7233  oelim2  7234  omsmolem  7292  fisucdomOLD  7713  ssnnfi  7729  fiint  7786  unifi  7798  indexfi  7817  iinfi  7866  unwdomg  7999  inf3lem5  8038  rankr1bg  8210  rankr1c  8228  carden2a  8336  dfac8clem  8402  dfac5lem4  8496  pwsdompw  8573  cfsuc  8626  cflim2  8632  enfin2i  8690  isf34lem4  8746  axdc4lem  8824  zornn0g  8874  uniimadomf  8909  fpwwe2lem8  9004  fpwwe2lem12  9008  fpwwe2lem13  9009  pwfseqlem1  9025  pwfseqlem5  9030  intgru  9181  addclpi  9259  addnidpi  9268  ltsonq  9336  nqpr  9381  reclem3pr  9416  recexsr  9473  supsrlem  9477  infmrcl  10511  nnnn0addcl  10815  un0addcl  10818  un0mulcl  10819  nn0nndivcl  10852  nn0ge0div  10919  uzind3  10943  uzind3OLD  10945  uzind4  11128  zsupss  11160  rpnnen1lem1  11197  rpnnen1lem2  11198  rpnnen1lem3  11199  rpnnen1lem5  11201  ltsubrp  11240  ltaddrp  11241  xrlttr  11335  qbtwnxr  11388  xltnegi  11404  xaddnemnf  11422  xaddnepnf  11423  xaddcom  11426  xnegdi  11429  xsubge0  11442  xrub  11492  fzind2  11881  seqof  12120  expp1  12129  expneg  12130  expcllem  12133  mulexpz  12161  expaddz  12165  expmulz  12167  faclbnd4lem3  12328  faclbnd4  12330  brfi1uzind  12485  swrd00  12595  swrd0  12608  cats1un  12651  reuccats1  12656  cshw0  12715  cshwn  12718  wwlktovfo  12846  shftf  12862  sqrdiv  13049  leabs  13082  mulcn2  13367  summolem2  13487  fsumrev2  13546  geomulcvg  13637  ruclem6  13818  dvdseq  13881  dvdsfac  13889  gcdcllem1  13997  rpexp1i  14110  hashdvds  14153  iserodd  14207  pcqcl  14228  pcid  14244  ismred  14846  funcpropd  15116  natpropd  15192  lubun  15599  odupos  15611  issubmd  15783  grpinvnzcl  15904  mulgneg  15953  mulgnn0z  15955  symgfixf1  16251  symgsssg  16281  symgfisg  16282  pgpssslw  16423  sylow2alem2  16427  sylow2a  16428  oddvdssubg  16647  gsumzunsnd  16766  gsumunsnfd  16767  gsum2dlem1  16781  gsum2dlem2  16782  gsum2dOLD  16784  ablfac1eu  16907  pgpfac1lem5  16913  gsumdixpOLD  17034  gsumdixp  17035  dvdsrcl2  17076  isdrngd  17197  evlslem4OLD  17937  evlslem4  17938  coe1tmmul2  18081  cnsubrg  18239  psgnodpm  18384  gsumcom3  18661  cpmidpmat  19134  intcld  19300  neiptopnei  19392  ordtrest2lem  19463  lmss  19558  cmpcovf  19650  cncmp  19651  fincmp  19652  cmpsublem  19658  cmpsub  19659  uncon  19689  1stcfb  19705  2ndcsep  19719  1stckgenlem  19782  ptbasin  19806  ptbasfi  19810  ptunimpt  19824  ptuniconst  19827  dfac14  19847  ptcnp  19851  xkoptsub  19883  xkococnlem  19888  xkoinjcn  19916  qtopcmplem  19936  qtophmeo  20046  fbfinnfr  20070  isfcls  20238  psmettri2  20541  xmetrtri  20586  xmetrtri2  20587  blssioo  21028  divcn  21100  bndth  21186  resscdrg  21526  minveclem3  21572  finiunmbl  21682  opnmbllem  21738  ismbf2d  21776  itg2seq  21877  ellimc2  22009  limcmpt2  22016  limcres  22018  dvlem  22028  dvidlem  22047  dvrec  22086  dveflem  22108  dvlip  22122  coe1mul3  22228  dvtaylp  22492  leibpilem2  22993  leibpi  22994  wilthlem2  23064  basellem3  23077  dvdsflip  23179  dchreq  23254  dchrsum  23265  lgsval3  23310  lgsdir2lem4  23322  2sqlem6  23365  rpvmasumlem  23393  dchrisum0fno1  23417  rpvmasum2  23418  pntrsumbnd2  23473  ostthlem1  23533  colmid  23766  lmiisolem  23831  axcontlem2  23937  axcontlem7  23942  umgraex  23986  usgraidx2vlem1  24053  nbgraf1olem3  24105  nbgraf1olem5  24107  cusconngra  24338  wlknwwlknfun  24372  wlknwwlkninj  24373  wlknwwlknsur  24374  wlkiswwlkfun  24379  wlkiswwlkinj  24380  wlkiswwlksur  24381  wwlkextfun  24391  wwlkextsur  24393  wlkv0  24422  clwwlkf  24456  grpoidinvlem3  24734  ablo32  24814  ablomuldiv  24817  ablodivdiv  24818  ablodiv32  24820  nvadd12  25042  nvscom  25050  nvsubsub23  25083  dipassr  25287  htthlem  25360  hsn0elch  25692  shscli  25761  nmopun  26459  branmfn  26550  mdslj1i  26764  mdslj2i  26765  atss  26791  chcv1  26800  dmdbr5ati  26867  fcnvgreu  27036  isoun  27042  ordtrest2NEWlem  27390  esumsplit  27553  esumpcvgval  27574  sigaclcu2  27610  volmeas  27693  mbfmco2  27726  oddpwdc  27783  eulerpartlemgvv  27805  ballotlemfc0  27921  ballotlemfcc  27922  subfacp1lem4  28117  erdszelem7  28131  erdszelem8  28132  erdsze2lem2  28138  rescon  28181  cvmsdisj  28205  cvmscld  28208  climuzcnv  28362  prodmolem2  28494  zprod  28496  prodsn  28519  pocnv  28620  trpredmintr  28741  cgrid2  29080  btwncom  29091  btwnswapid2  29095  colinearperm1  29139  colinearperm3  29140  colinearperm2  29141  colinearperm4  29142  lineext  29153  colinbtwnle  29195  broutsideof2  29199  outsideofcom  29205  linecom  29227  linerflx2  29228  lineintmo  29234  bpolydiflem  29243  bpoly2  29246  bpoly3  29247  hfext  29267  fin2solem  29466  opnmbllem0  29478  mblfinlem3  29481  mbfposadd  29490  itg2addnclem3  29496  bddiblnc  29513  ftc1anclem6  29523  ftc1anc  29526  ntruni  29573  clsint2  29575  locfincmp  29627  neibastop1  29631  eqfnun  29666  ac6gf  29677  heibor1lem  29759  isdrngo2  29815  unichnidl  29882  isfldidl  29919  ismrcd1  30085  isnacs3  30097  pellfundglb  30276  jm2.22  30394  jm2.23  30395  isnumbasgrplem1  30507  hbtlem6  30535  rngunsnply  30580  hashgcdlem  30615  phisum  30617  afv0nbfvbi  31522  usgedgppr  31664  usgpredgv  31665  usgpredgvALT  31666  edgssv2ALT  31667  edgssv2  31668  usgedgvadf1lem1  31679  usgedgvadf1ALTlem1  31682  lspsslco  31986  bnj521  32747  bnj1109  32799  bnj1294  32830  bnj545  32907  bnj605  32919  bnj594  32924  bnj934  32947  bnj953  32951  bnj1137  33005  bnj1174  33013  bnj1388  33043  bj-snsetex  33477  lkrss2N  33841  elpadd0  34480  ltrnu  34792  tendoex  35646  cdlemm10N  35790  dicfnN  35855  dihmeetlem2N  35971  dihlatat  36009  lcfrlem9  36222