Theorem sylan2b 483

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

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376

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 190  df-an 378

This theorem is referenced by:  syl2anb  487  eupickb  2387  eqtr3  2492  elnelne1  2753  elnelne2  2754  morex  3210  psssstr  3525  reuss2  3714  reupick  3718  reximdva0  3734  rabsneu  4038  opabss  4457  triun  4503  poirr  4771  wefrc  4833  xpcan  5279  fnfco  5760  fnressn  6092  fvtp3  6129  fvtp3g  6132  f1mpt  6180  offval  6557  ordsucuniel  6670  onzsl  6692  soex  6755  fun11iun  6772  dfoprab3  6868  1stconst  6903  2ndconst  6904  poxp  6927  fnwelem  6930  suppssr  6965  suppsssn  6969  oeordsuc  7313  oelim2  7314  omsmolem  7372  ssnnfi  7809  fiint  7866  unifi  7881  indexfi  7900  iinfi  7949  unwdomg  8117  inf3lem5  8155  rankr1bg  8292  rankr1c  8310  carden2a  8418  dfac8clem  8481  dfac5lem4  8575  pwsdompw  8652  cfsuc  8705  cflim2  8711  enfin2i  8769  isf34lem4  8825  axdc4lem  8903  zornn0g  8953  uniimadomf  8988  fpwwe2lem8  9080  fpwwe2lem12  9084  fpwwe2lem13  9085  pwfseqlem1  9101  pwfseqlem5  9106  intgru  9257  addclpi  9335  addnidpi  9344  ltsonq  9412  nqpr  9457  reclem3pr  9492  recexsr  9549  supsrlem  9553  infmrclOLD  10615  nnnn0addcl  10924  un0addcl  10927  un0mulcl  10928  nn0nndivcl  10960  nn0ge0div  11028  uzind3  11052  uzind4  11240  zsupss  11276  rpnnen1lem1  11313  rpnnen1lem2  11314  rpnnen1lem3  11315  rpnnen1lem5  11317  ltsubrp  11358  ltaddrp  11359  xrlttr  11462  qbtwnxr  11516  xltnegi  11532  xaddnemnf  11551  xaddnepnf  11552  xaddcom  11555  xnegdi  11559  xsubge0  11572  xrub  11622  fzind2  12054  seqof  12308  expp1  12317  expneg  12318  expcllem  12321  mulexpz  12350  expaddz  12354  expmulz  12356  faclbnd4lem3  12518  faclbnd4  12520  fi1uzind  12691  fi1uzindOLD  12697  swrd00  12828  swrd0  12844  cats1un  12886  reuccats1  12891  cshw0  12950  cshwn  12953  wwlktovfo  13108  shftf  13219  sqrtdiv  13406  leabs  13439  mulcn2  13736  summolem2  13859  fsumrev2  13920  geomulcvg  14009  prodmolem2  14066  zprod  14068  prodsn  14093  prodsnf  14095  bpolydiflem  14184  bpoly2  14187  bpoly3  14188  ruclem6  14364  dvdseq  14429  dvdsfac  14438  gcdcllem1  14552  lcmgcdlem  14650  rpexp1i  14752  hashdvds  14802  iserodd  14864  pcqcl  14885  pcid  14901  ismred  15586  funcpropd  15883  natpropd  15959  lubun  16447  odupos  16459  issubmd  16674  grpinvnzcl  16804  mulgneg  16854  mulgnn0z  16856  symgfixf1  17156  symgsssg  17186  symgfisg  17187  pgpssslw  17344  sylow2alem2  17348  sylow2a  17349  oddvdssubg  17571  gsumzunsnd  17666  gsumunsnfd  17667  gsum2dlem1  17680  gsum2dlem2  17681  ablfac1eu  17784  pgpfac1lem5  17790  gsumdixp  17915  dvdsrcl2  17956  isdrngd  18078  evlslem4  18808  coe1tmmul2  18946  cnsubrg  19105  psgnodpm  19233  gsumcom3  19501  mpt2matmul  19548  cpmidpmat  19974  intcld  20132  neiptopnei  20225  ordtrest2lem  20296  lmss  20391  cmpcovf  20483  cncmp  20484  fincmp  20485  cmpsublem  20491  cmpsub  20492  uncon  20521  1stcfb  20537  2ndcsep  20551  refun0  20607  locfincmp  20618  1stckgenlem  20645  ptbasin  20669  ptbasfi  20673  ptunimpt  20687  ptuniconst  20690  dfac14  20710  ptcnp  20714  xkoptsub  20746  xkococnlem  20751  xkoinjcn  20779  qtopcmplem  20799  qtophmeo  20909  fbfinnfr  20934  isufil2  21001  isfcls  21102  xmetrtri  21448  xmetrtri2  21449  blssioo  21891  divcn  21978  bndth  22064  resscdrg  22403  minveclem3  22449  minveclem3OLD  22461  finiunmbl  22576  opnmbllem  22638  ismbf2d  22676  itg2seq  22779  ellimc2  22911  limcmpt2  22918  limcres  22920  dvlem  22930  dvidlem  22949  dvrec  22988  dveflem  23010  dvlip  23024  coe1mul3  23127  dvtaylp  23404  leibpilem2  23946  leibpi  23947  wilthlem2  24073  basellem3  24088  dvdsflip  24190  dchreq  24265  dchrsum  24276  lgsval3  24321  lgsdir2lem4  24333  2sqlem6  24376  rpvmasumlem  24404  dchrisum0fno1  24428  rpvmasum2  24429  pntrsumbnd2  24484  ostthlem1  24544  colmid  24812  lmiisolem  24917  dfcgra2  24950  axcontlem2  25074  axcontlem7  25079  umgraex  25129  usgraidx2vlem1  25197  nbgraf1olem3  25250  nbgraf1olem5  25252  cusconngra  25483  wlknwwlknfun  25517  wlknwwlkninj  25518  wlknwwlknsur  25519  wlkiswwlkfun  25524  wlkiswwlkinj  25525  wlkiswwlksur  25526  wwlkextfun  25536  wwlkextsur  25538  wlkv0  25567  clwwlkf  25601  grpoidinvlem3  26015  ablo32  26095  ablomuldiv  26098  ablodivdiv  26099  ablodiv32  26101  nvadd12  26323  nvscom  26331  nvsubsub23  26364  dipassr  26568  htthlem  26651  hsn0elch  26982  shscli  27051  nmopun  27748  branmfn  27839  mdslj1i  28053  mdslj2i  28054  atss  28080  chcv1  28089  dmdbr5ati  28156  fcnvgreu  28350  isoun  28357  ordtrest2NEWlem  28802  esumsplit  28948  esumpad2  28951  esumpcvgval  28973  sigaclcu2  29016  ldgenpisyslem1  29059  volmeas  29127  mbfmco2  29160  omsmeas  29228  omsmeasOLD  29229  oddpwdc  29260  eulerpartlemgvv  29282  ballotlemfc0  29398  ballotlemfcc  29399  bnj521  29617  bnj1109  29670  bnj1294  29701  bnj545  29778  bnj605  29790  bnj594  29795  bnj934  29818  bnj953  29822  bnj1137  29876  bnj1174  29884  bnj1388  29914  subfacp1lem4  29978  erdszelem7  29992  erdszelem8  29993  erdsze2lem2  29999  rescon  30041  cvmsdisj  30065  cvmscld  30068  mclsax  30279  climuzcnv  30387  pocnv  30475  trpredmintr  30543  cgrid2  30841  btwncom  30852  btwnswapid2  30856  colinearperm1  30900  colinearperm3  30901  colinearperm2  30902  colinearperm4  30903  lineext  30914  colinbtwnle  30956  broutsideof2  30960  outsideofcom  30966  linecom  30988  linerflx2  30989  lineintmo  30995  fwddifn0  31002  hfext  31021  ntruni  31054  clsint2  31056  neibastop1  31086  bj-snsetex  31627  relowlssretop  31836  fin2solem  31995  poimirlem4  32008  poimirlem25  32029  poimirlem32  32036  opnmbllem0  32040  mblfinlem3  32043  mbfposadd  32052  itg2addnclem3  32059  bddiblnc  32076  ftc1anclem6  32086  ftc1anc  32089  eqfnun  32112  ac6gf  32123  heibor1lem  32205  isdrngo2  32261  unichnidl  32328  isfldidl  32365  cnf1dd  32390  lkrss2N  32806  elpadd0  33445  ltrnu  33757  tendoex  34613  cdlemm10N  34757  dicfnN  34822  dihmeetlem2N  34938  dihlatat  34976  lcfrlem9  35189  ismrcd1  35611  isnacs3  35623  pellfundglb  35804  jm2.22  35921  jm2.23  35922  isnumbasgrplem1  36031  hbtlem6  36059  rngunsnply  36110  hashgcdlem  36145  phisum  36147  dvgrat  36731  cvgdvgrat  36732  nznngen  36735  uzmptshftfval  36765  iccshift  37715  iooshift  37719  itgperiod  37955  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem68  38150  fourierdlem93  38175  elprneb  38857  falseral0  39133  upgrex  39338  umgredg  39390  umgrpredgav  39391  umgredgne  39394  usgredgappr  39441  edgassv2  39443  uspgredg2vlem  39464  usgredg2vlem1  39466  upgrres1  39544  nbuhgr2vtx1edgblem  39583  nbusgrf1o0  39607  hashnbusgrnn0  39614  iscplgredg  39649  uhgrvd00  39757  1wlkepvtx  39858  usgedgppr  40218  usgpredgv  40219  usgpredgvALT  40220  edgssv2ALT  40221  edgssv2  40222  usgedgvadf1lem1  40233  usgedgvadf1ALTlem1  40236  rabsubmgmd  40299  2zlidl  40442  lspsslco  40738