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  965  eupickb  2344  bm1.1OLD  2425  eqtr3  2469  elnelne1  2788  elnelne2  2789  morex  3267  psssstr  3592  reuss2  3760  reupick  3764  reximdva0  3778  rabsneu  4086  opabss  4494  triun  4539  poirr  4797  wefrc  4859  xpcan  5429  fnfco  5736  suppssrOLD  6002  fnressn  6064  fvtp3  6101  fvtp3g  6104  f1mpt  6150  offval  6528  ordsucuniel  6640  onzsl  6662  soex  6724  fun11iun  6741  dfoprab3  6837  1stconst  6869  2ndconst  6870  poxp  6893  fnwelem  6896  suppssr  6929  suppsssn  6933  oeordsuc  7241  oelim2  7242  omsmolem  7300  fisucdomOLD  7721  ssnnfi  7737  fiint  7795  unifi  7807  indexfi  7826  iinfi  7875  unwdomg  8008  inf3lem5  8047  rankr1bg  8219  rankr1c  8237  carden2a  8345  dfac8clem  8411  dfac5lem4  8505  pwsdompw  8582  cfsuc  8635  cflim2  8641  enfin2i  8699  isf34lem4  8755  axdc4lem  8833  zornn0g  8883  uniimadomf  8918  fpwwe2lem8  9013  fpwwe2lem12  9017  fpwwe2lem13  9018  pwfseqlem1  9034  pwfseqlem5  9039  intgru  9190  addclpi  9268  addnidpi  9277  ltsonq  9345  nqpr  9390  reclem3pr  9425  recexsr  9482  supsrlem  9486  infmrcl  10523  nnnn0addcl  10827  un0addcl  10830  un0mulcl  10831  nn0nndivcl  10864  nn0ge0div  10933  uzind3  10957  uzind3OLD  10959  uzind4  11143  zsupss  11175  rpnnen1lem1  11212  rpnnen1lem2  11213  rpnnen1lem3  11214  rpnnen1lem5  11216  ltsubrp  11255  ltaddrp  11256  xrlttr  11350  qbtwnxr  11403  xltnegi  11419  xaddnemnf  11437  xaddnepnf  11438  xaddcom  11441  xnegdi  11444  xsubge0  11457  xrub  11507  fzind2  11898  seqof  12138  expp1  12147  expneg  12148  expcllem  12151  mulexpz  12180  expaddz  12184  expmulz  12186  faclbnd4lem3  12347  faclbnd4  12349  brfi1uzind  12506  swrd00  12619  swrd0  12632  cats1un  12675  reuccats1  12680  cshw0  12739  cshwn  12742  wwlktovfo  12870  shftf  12886  sqrtdiv  13073  leabs  13106  mulcn2  13392  summolem2  13512  fsumrev2  13571  geomulcvg  13659  ruclem6  13840  dvdseq  13905  dvdsfac  13913  gcdcllem1  14021  rpexp1i  14134  hashdvds  14177  iserodd  14231  pcqcl  14252  pcid  14268  ismred  14871  funcpropd  15138  natpropd  15214  lubun  15622  odupos  15634  issubmd  15849  grpinvnzcl  15979  mulgneg  16029  mulgnn0z  16031  symgfixf1  16331  symgsssg  16361  symgfisg  16362  pgpssslw  16503  sylow2alem2  16507  sylow2a  16508  oddvdssubg  16730  gsumzunsnd  16851  gsumunsnfd  16852  gsum2dlem1  16866  gsum2dlem2  16867  gsum2dOLD  16869  ablfac1eu  16992  pgpfac1lem5  16998  gsumdixpOLD  17125  gsumdixp  17126  dvdsrcl2  17167  isdrngd  17289  evlslem4OLD  18041  evlslem4  18042  coe1tmmul2  18185  cnsubrg  18346  psgnodpm  18491  gsumcom3  18768  mpt2matmul  18815  cpmidpmat  19241  intcld  19407  neiptopnei  19499  ordtrest2lem  19570  lmss  19665  cmpcovf  19757  cncmp  19758  fincmp  19759  cmpsublem  19765  cmpsub  19766  uncon  19796  1stcfb  19812  2ndcsep  19826  refun0  19882  locfincmp  19893  1stckgenlem  19920  ptbasin  19944  ptbasfi  19948  ptunimpt  19962  ptuniconst  19965  dfac14  19985  ptcnp  19989  xkoptsub  20021  xkococnlem  20026  xkoinjcn  20054  qtopcmplem  20074  qtophmeo  20184  fbfinnfr  20208  isufil2  20275  isfcls  20376  xmetrtri  20724  xmetrtri2  20725  blssioo  21166  divcn  21238  bndth  21324  resscdrg  21664  minveclem3  21710  finiunmbl  21820  opnmbllem  21876  ismbf2d  21914  itg2seq  22015  ellimc2  22147  limcmpt2  22154  limcres  22156  dvlem  22166  dvidlem  22185  dvrec  22224  dveflem  22246  dvlip  22260  coe1mul3  22366  dvtaylp  22630  leibpilem2  23137  leibpi  23138  wilthlem2  23208  basellem3  23221  dvdsflip  23323  dchreq  23398  dchrsum  23409  lgsval3  23454  lgsdir2lem4  23466  2sqlem6  23509  rpvmasumlem  23537  dchrisum0fno1  23561  rpvmasum2  23562  pntrsumbnd2  23617  ostthlem1  23677  colmid  23930  lmiisolem  24026  axcontlem2  24133  axcontlem7  24138  umgraex  24188  usgraidx2vlem1  24256  nbgraf1olem3  24308  nbgraf1olem5  24310  cusconngra  24541  wlknwwlknfun  24575  wlknwwlkninj  24576  wlknwwlknsur  24577  wlkiswwlkfun  24582  wlkiswwlkinj  24583  wlkiswwlksur  24584  wwlkextfun  24594  wwlkextsur  24596  wlkv0  24625  clwwlkf  24659  grpoidinvlem3  25073  ablo32  25153  ablomuldiv  25156  ablodivdiv  25157  ablodiv32  25159  nvadd12  25381  nvscom  25389  nvsubsub23  25422  dipassr  25626  htthlem  25699  hsn0elch  26031  shscli  26100  nmopun  26798  branmfn  26889  mdslj1i  27103  mdslj2i  27104  atss  27130  chcv1  27139  dmdbr5ati  27206  fcnvgreu  27379  isoun  27385  ordtrest2NEWlem  27770  esumsplit  27929  esumpcvgval  27950  sigaclcu2  27986  volmeas  28069  mbfmco2  28102  oddpwdc  28159  eulerpartlemgvv  28181  ballotlemfc0  28297  ballotlemfcc  28298  subfacp1lem4  28493  erdszelem7  28507  erdszelem8  28508  erdsze2lem2  28514  rescon  28557  cvmsdisj  28581  cvmscld  28584  mclsax  28795  climuzcnv  28903  prodmolem2  29035  zprod  29037  prodsn  29060  pocnv  29161  trpredmintr  29282  cgrid2  29621  btwncom  29632  btwnswapid2  29636  colinearperm1  29680  colinearperm3  29681  colinearperm2  29682  colinearperm4  29683  lineext  29694  colinbtwnle  29736  broutsideof2  29740  outsideofcom  29746  linecom  29768  linerflx2  29769  lineintmo  29775  bpolydiflem  29784  bpoly2  29787  bpoly3  29788  hfext  29808  fin2solem  30007  opnmbllem0  30018  mblfinlem3  30021  mbfposadd  30030  itg2addnclem3  30036  bddiblnc  30053  ftc1anclem6  30063  ftc1anc  30066  ntruni  30113  clsint2  30115  neibastop1  30145  eqfnun  30180  ac6gf  30191  heibor1lem  30273  isdrngo2  30329  unichnidl  30396  isfldidl  30433  cnf1dd  30458  ismrcd1  30598  isnacs3  30610  pellfundglb  30789  jm2.22  30905  jm2.23  30906  isnumbasgrplem1  31018  hbtlem6  31046  rngunsnply  31091  hashgcdlem  31126  phisum  31128  dvgrat  31162  cvgdvgrat  31163  lcmgcdlem  31181  nznngen  31190  iccshift  31490  iooshift  31494  itgperiod  31666  fourierdlem42  31816  fourierdlem68  31842  fourierdlem93  31867  usgedgppr  32232  usgpredgv  32233  usgpredgvALT  32234  edgssv2ALT  32235  edgssv2  32236  usgedgvadf1lem1  32247  usgedgvadf1ALTlem1  32250  rabsubmgmd  32313  2zlidl  32440  lspsslco  32748  bnj521  33500  bnj1109  33552  bnj1294  33583  bnj545  33660  bnj605  33672  bnj594  33677  bnj934  33700  bnj953  33704  bnj1137  33758  bnj1174  33766  bnj1388  33796  bj-snsetex  34233  lkrss2N  34596  elpadd0  35235  ltrnu  35547  tendoex  36403  cdlemm10N  36547  dicfnN  36612  dihmeetlem2N  36728  dihlatat  36766  lcfrlem9  36979