Theorem sylan2b 462

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

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359

This theorem is referenced by:  syl2anb  466  bm1.1  2389  eqtr3  2423  morex  3078  psssstr  3413  reuss2  3581  reupick  3585  reximdva0  3599  rabsneu  3839  opabss  4229  triun  4275  poirr  4474  wefrc  4536  ordsucuniel  4763  onzsl  4785  xpcan  5264  soex  5278  fnfco  5568  fun11iun  5654  suppssr  5823  eldmrexrnb  5836  fnressn  5877  fvtp3  5900  fvtp3g  5903  f1mpt  5966  offval  6271  dfoprab3  6362  1stconst  6394  2ndconst  6395  poxp  6417  fnwelem  6420  tfrlem2  6596  oeordsuc  6796  oelim2  6797  omsmolem  6855  fisucdomOLD  7271  ssnnfi  7287  fiint  7342  unifi  7354  indexfi  7372  iinfi  7380  unwdomg  7508  inf3lem5  7543  rankr1bg  7685  rankr1c  7703  carden2a  7809  dfac8clem  7869  dfac5lem4  7963  pwsdompw  8040  cfsuc  8093  cflim2  8099  enfin2i  8157  isf34lem4  8213  axdc4lem  8291  zornn0g  8341  uniimadomf  8376  fpwwe2lem8  8468  fpwwe2lem12  8472  fpwwe2lem13  8473  pwfseqlem1  8489  pwfseqlem5  8494  intgru  8645  addclpi  8725  addnidpi  8734  ltsonq  8802  nqpr  8847  reclem3pr  8882  recexsr  8938  supsrlem  8942  infmrcl  9943  nnnn0addcl  10207  un0addcl  10209  un0mulcl  10210  uzind3  10319  uzind3OLD  10321  uzind4  10490  zsupss  10521  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem5  10560  ltsubrp  10599  ltaddrp  10600  xrlttr  10689  qbtwnxr  10742  xltnegi  10758  xaddnemnf  10776  xaddnepnf  10777  xaddcom  10780  xnegdi  10783  xsubge0  10796  xrub  10846  fzind2  11153  seqof  11335  expp1  11343  expneg  11344  expcllem  11347  mulexpz  11375  expaddz  11379  expmulz  11381  faclbnd4lem3  11541  faclbnd4  11543  brfi1uzind  11670  swrd00  11720  cats1un  11745  shftf  11849  sqrdiv  12026  leabs  12059  mulcn2  12344  summolem2  12465  fsumrev2  12520  geomulcvg  12608  ruclem6  12789  dvdseq  12852  dvdsfac  12859  gcdcllem1  12966  rpexp1i  13076  hashdvds  13119  iserodd  13164  pcqcl  13185  pcid  13201  ismred  13782  funcpropd  14052  natpropd  14128  latlem12  14462  clatl  14498  lubun  14505  odupos  14517  grpinvnzcl  14818  mulgneg  14863  mulgnn0z  14865  pgpssslw  15203  sylow2alem2  15207  sylow2a  15208  oddvdssubg  15425  gsumunsn  15499  gsum2d  15501  ablfac1eu  15586  pgpfac1lem5  15592  gsumdixp  15670  dvdsrcl2  15710  isdrngd  15815  evlslem4  16519  coe1tmmul2  16623  cnsubrg  16714  intcld  17059  neiptopnei  17151  ordtrest2lem  17221  lmss  17316  cmpcovf  17408  cncmp  17409  fincmp  17410  cmpsublem  17416  cmpsub  17417  uncon  17445  1stcfb  17461  2ndcsep  17475  1stckgenlem  17538  ptbasin  17562  ptbasfi  17566  ptunimpt  17580  ptuniconst  17583  dfac14  17603  ptcnp  17607  xkoptsub  17639  xkococnlem  17644  xkoinjcn  17672  qtopcmplem  17692  qtophmeo  17802  fbfinnfr  17826  isfcls  17994  psmettri2  18293  xmetrtri  18338  xmetrtri2  18339  blssioo  18779  divcn  18851  bndth  18936  resscdrg  19265  minveclem3  19283  finiunmbl  19391  opnmbllem  19446  ismbf2d  19486  itg2seq  19587  ellimc2  19717  limcmpt2  19724  limcres  19726  dvlem  19736  dvidlem  19755  dvrec  19794  dveflem  19816  dvlip  19830  coe1mul3  19975  dvtaylp  20239  leibpilem2  20734  leibpi  20735  wilthlem2  20805  basellem3  20818  dvdsflip  20920  dchreq  20995  dchrsum  21006  lgsval3  21051  lgsdir2lem4  21063  2sqlem6  21106  rpvmasumlem  21134  dchrisum0fno1  21158  rpvmasum2  21159  pntrsumbnd2  21214  ostthlem1  21274  umgraex  21311  usgraidx2vlem1  21363  nbgraf1olem3  21406  nbgraf1olem5  21408  cusconngra  21616  grpoidinvlem3  21747  ablo32  21827  ablomuldiv  21830  ablodivdiv  21831  ablodiv32  21833  nvadd12  22055  nvscom  22063  nvsubsub23  22096  dipassr  22300  htthlem  22373  hsn0elch  22703  shscli  22772  nmopun  23470  branmfn  23561  mdslj1i  23775  mdslj2i  23776  atss  23802  chcv1  23811  dmdbr5ati  23878  isoun  24042  esumsplit  24400  esumpcvgval  24421  sigaclcu2  24456  volmeas  24540  mbfmco2  24568  ballotlemfc0  24703  ballotlemfcc  24704  subfacp1lem4  24822  erdszelem7  24836  erdszelem8  24837  erdsze2lem2  24843  rescon  24886  cvmsdisj  24910  cvmscld  24913  climuzcnv  25061  prodmolem2  25214  zprod  25216  prodsn  25239  trpredmintr  25448  axcontlem2  25808  axcontlem7  25813  cgrid2  25841  btwncom  25852  btwnswapid2  25856  colinearperm1  25900  colinearperm3  25901  colinearperm2  25902  colinearperm4  25903  lineext  25914  colinbtwnle  25956  broutsideof2  25960  outsideofcom  25966  linecom  25988  linerflx2  25989  lineintmo  25995  bpolydiflem  26004  bpoly2  26007  bpoly3  26008  hfext  26028  mblfinlem2  26144  mbfposadd  26153  itg2addnclem3  26157  bddiblnc  26174  ntruni  26220  clsint2  26222  locfincmp  26274  neibastop1  26278  eqfnun  26313  ac6gf  26324  heibor1lem  26408  isdrngo2  26464  unichnidl  26531  isfldidl  26568  ismrcd1  26642  isnacs3  26654  pellfundglb  26838  jm2.22  26956  jm2.23  26957  isnumbasgrplem1  27134  hbtlem6  27201  rngunsnply  27246  issubmd  27251  symgsssg  27276  symgfisg  27277  gsumcom3  27322  hashgcdlem  27384  phisum  27386  afv0nbfvbi  27882  bnj521  28810  bnj926  28844  bnj1109  28863  bnj1294  28895  bnj545  28972  bnj605  28984  bnj594  28989  bnj934  29012  bnj953  29016  bnj1137  29070  bnj1174  29078  bnj1388  29108  lubunNEW  29456  lkrss2N  29652  elpadd0  30291  ltrnu  30603  tendoex  31457  cdlemm10N  31601  dicfnN  31666  dihmeetlem2N  31782  dihlatat  31820  lcfrlem9  32033

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361