Theorem sylan2b 478

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 198	. 2 |- ( ph -> ch )
3		sylan2b.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 477	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  syl2anb  482  bianirOLD  978  eupickb  2366  eqtr3  2471  elnelne1  2733  elnelne2  2734  morex  3221  psssstr  3538  reuss2  3722  reupick  3726  reximdva0  3742  rabsneu  4046  opabss  4463  triun  4509  poirr  4765  wefrc  4827  xpcan  5272  fnfco  5746  fnressn  6074  fvtp3  6111  fvtp3g  6114  f1mpt  6160  offval  6535  ordsucuniel  6648  onzsl  6670  soex  6733  fun11iun  6750  dfoprab3  6846  1stconst  6881  2ndconst  6882  poxp  6905  fnwelem  6908  suppssr  6943  suppsssn  6947  oeordsuc  7292  oelim2  7293  omsmolem  7351  ssnnfi  7788  fiint  7845  unifi  7860  indexfi  7879  iinfi  7928  unwdomg  8096  inf3lem5  8134  rankr1bg  8271  rankr1c  8289  carden2a  8397  dfac8clem  8460  dfac5lem4  8554  pwsdompw  8631  cfsuc  8684  cflim2  8690  enfin2i  8748  isf34lem4  8804  axdc4lem  8882  zornn0g  8932  uniimadomf  8967  fpwwe2lem8  9059  fpwwe2lem12  9063  fpwwe2lem13  9064  pwfseqlem1  9080  pwfseqlem5  9085  intgru  9236  addclpi  9314  addnidpi  9323  ltsonq  9391  nqpr  9436  reclem3pr  9471  recexsr  9528  supsrlem  9532  infmrclOLD  10590  nnnn0addcl  10897  un0addcl  10900  un0mulcl  10901  nn0nndivcl  10933  nn0ge0div  11002  uzind3  11026  uzind4  11214  zsupss  11250  rpnnen1lem1  11287  rpnnen1lem2  11288  rpnnen1lem3  11289  rpnnen1lem5  11291  ltsubrp  11332  ltaddrp  11333  xrlttr  11436  qbtwnxr  11490  xltnegi  11506  xaddnemnf  11524  xaddnepnf  11525  xaddcom  11528  xnegdi  11531  xsubge0  11544  xrub  11594  fzind2  12020  seqof  12267  expp1  12276  expneg  12277  expcllem  12280  mulexpz  12309  expaddz  12313  expmulz  12315  faclbnd4lem3  12477  faclbnd4  12479  fi1uzind  12647  swrd00  12769  swrd0  12785  cats1un  12827  reuccats1  12832  cshw0  12891  cshwn  12894  wwlktovfo  13026  shftf  13135  sqrtdiv  13322  leabs  13355  mulcn2  13652  summolem2  13775  fsumrev2  13836  geomulcvg  13925  prodmolem2  13982  zprod  13984  prodsn  14009  prodsnf  14011  bpolydiflem  14100  bpoly2  14103  bpoly3  14104  ruclem6  14280  dvdseq  14345  dvdsfac  14353  gcdcllem1  14466  lcmgcdlem  14564  rpexp1i  14666  hashdvds  14716  iserodd  14778  pcqcl  14799  pcid  14815  ismred  15501  funcpropd  15798  natpropd  15874  lubun  16362  odupos  16374  issubmd  16589  grpinvnzcl  16719  mulgneg  16769  mulgnn0z  16771  symgfixf1  17071  symgsssg  17101  symgfisg  17102  pgpssslw  17259  sylow2alem2  17263  sylow2a  17264  oddvdssubg  17486  gsumzunsnd  17581  gsumunsnfd  17582  gsum2dlem1  17595  gsum2dlem2  17596  ablfac1eu  17699  pgpfac1lem5  17705  gsumdixp  17830  dvdsrcl2  17871  isdrngd  17993  evlslem4  18724  coe1tmmul2  18862  cnsubrg  19021  psgnodpm  19149  gsumcom3  19417  mpt2matmul  19464  cpmidpmat  19890  intcld  20048  neiptopnei  20141  ordtrest2lem  20212  lmss  20307  cmpcovf  20399  cncmp  20400  fincmp  20401  cmpsublem  20407  cmpsub  20408  uncon  20437  1stcfb  20453  2ndcsep  20467  refun0  20523  locfincmp  20534  1stckgenlem  20561  ptbasin  20585  ptbasfi  20589  ptunimpt  20603  ptuniconst  20606  dfac14  20626  ptcnp  20630  xkoptsub  20662  xkococnlem  20667  xkoinjcn  20695  qtopcmplem  20715  qtophmeo  20825  fbfinnfr  20849  isufil2  20916  isfcls  21017  xmetrtri  21363  xmetrtri2  21364  blssioo  21806  divcn  21893  bndth  21979  resscdrg  22318  minveclem3  22364  minveclem3OLD  22376  finiunmbl  22490  opnmbllem  22552  ismbf2d  22590  itg2seq  22693  ellimc2  22825  limcmpt2  22832  limcres  22834  dvlem  22844  dvidlem  22863  dvrec  22902  dveflem  22924  dvlip  22938  coe1mul3  23041  dvtaylp  23318  leibpilem2  23860  leibpi  23861  wilthlem2  23987  basellem3  24002  dvdsflip  24104  dchreq  24179  dchrsum  24190  lgsval3  24235  lgsdir2lem4  24247  2sqlem6  24290  rpvmasumlem  24318  dchrisum0fno1  24342  rpvmasum2  24343  pntrsumbnd2  24398  ostthlem1  24458  colmid  24726  lmiisolem  24831  dfcgra2  24864  axcontlem2  24988  axcontlem7  24993  umgraex  25043  usgraidx2vlem1  25111  nbgraf1olem3  25164  nbgraf1olem5  25166  cusconngra  25397  wlknwwlknfun  25431  wlknwwlkninj  25432  wlknwwlknsur  25433  wlkiswwlkfun  25438  wlkiswwlkinj  25439  wlkiswwlksur  25440  wwlkextfun  25450  wwlkextsur  25452  wlkv0  25481  clwwlkf  25515  grpoidinvlem3  25927  ablo32  26007  ablomuldiv  26010  ablodivdiv  26011  ablodiv32  26013  nvadd12  26235  nvscom  26243  nvsubsub23  26276  dipassr  26480  htthlem  26563  hsn0elch  26894  shscli  26963  nmopun  27660  branmfn  27751  mdslj1i  27965  mdslj2i  27966  atss  27992  chcv1  28001  dmdbr5ati  28068  fcnvgreu  28268  isoun  28275  ordtrest2NEWlem  28721  esumsplit  28867  esumpad2  28870  esumpcvgval  28892  sigaclcu2  28935  ldgenpisyslem1  28978  volmeas  29047  mbfmco2  29080  omsmeas  29148  omsmeasOLD  29149  oddpwdc  29180  eulerpartlemgvv  29202  ballotlemfc0  29318  ballotlemfcc  29319  bnj521  29538  bnj1109  29591  bnj1294  29622  bnj545  29699  bnj605  29711  bnj594  29716  bnj934  29739  bnj953  29743  bnj1137  29797  bnj1174  29805  bnj1388  29835  subfacp1lem4  29899  erdszelem7  29913  erdszelem8  29914  erdsze2lem2  29920  rescon  29962  cvmsdisj  29986  cvmscld  29989  mclsax  30200  climuzcnv  30308  pocnv  30397  trpredmintr  30465  cgrid2  30763  btwncom  30774  btwnswapid2  30778  colinearperm1  30822  colinearperm3  30823  colinearperm2  30824  colinearperm4  30825  lineext  30836  colinbtwnle  30878  broutsideof2  30882  outsideofcom  30888  linecom  30910  linerflx2  30911  lineintmo  30917  fwddifn0  30924  hfext  30943  ntruni  30976  clsint2  30978  neibastop1  31008  bj-snsetex  31550  relowlssretop  31759  fin2solem  31924  poimirlem4  31937  poimirlem25  31958  poimirlem32  31965  opnmbllem0  31969  mblfinlem3  31972  mbfposadd  31981  itg2addnclem3  31988  bddiblnc  32005  ftc1anclem6  32015  ftc1anc  32018  eqfnun  32041  ac6gf  32052  heibor1lem  32134  isdrngo2  32190  unichnidl  32257  isfldidl  32294  cnf1dd  32319  lkrss2N  32729  elpadd0  33368  ltrnu  33680  tendoex  34536  cdlemm10N  34680  dicfnN  34745  dihmeetlem2N  34861  dihlatat  34899  lcfrlem9  35112  ismrcd1  35534  isnacs3  35546  pellfundglb  35727  jm2.22  35844  jm2.23  35845  isnumbasgrplem1  35954  hbtlem6  35982  rngunsnply  36033  hashgcdlem  36068  phisum  36070  dvgrat  36655  cvgdvgrat  36656  nznngen  36659  uzmptshftfval  36689  iccshift  37613  iooshift  37617  itgperiod  37852  fourierdlem42  38006  fourierdlem42OLD  38007  fourierdlem68  38032  fourierdlem93  38057  elprneb  38706  falseral0  38980  upgrex  39170  umgredg  39215  umgrpredgav  39216  umgredgne  39219  usgredgappr  39265  edgassv2  39267  uspgredg2vlem  39286  usgredg2vlem1  39288  upgrres1  39363  nbuhgr2vtx1edgblem  39402  nbusgrf1o0  39426  hashnbusgrnn0  39433  iscplgredg  39468  uhgrvd00  39554  usgedgppr  39697  usgpredgv  39698  usgpredgvALT  39699  edgssv2ALT  39700  edgssv2  39701  usgedgvadf1lem1  39712  usgedgvadf1ALTlem1  39715  rabsubmgmd  39778  2zlidl  39921  lspsslco  40217