Theorem sylan2b 477

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

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  syl2anb  481  bianirOLD  976  eupickb  2334  bm1.1OLD  2406  eqtr3  2450  elnelne1  2772  elnelne2  2773  morex  3255  psssstr  3571  reuss2  3753  reupick  3757  reximdva0  3773  rabsneu  4072  opabss  4482  triun  4528  poirr  4782  wefrc  4844  xpcan  5289  fnfco  5762  fnressn  6088  fvtp3  6125  fvtp3g  6128  f1mpt  6174  offval  6549  ordsucuniel  6662  onzsl  6684  soex  6747  fun11iun  6764  dfoprab3  6860  1stconst  6892  2ndconst  6893  poxp  6916  fnwelem  6919  suppssr  6954  suppsssn  6958  oeordsuc  7300  oelim2  7301  omsmolem  7359  ssnnfi  7794  fiint  7851  unifi  7866  indexfi  7885  iinfi  7934  unwdomg  8102  inf3lem5  8140  rankr1bg  8276  rankr1c  8294  carden2a  8402  dfac8clem  8464  dfac5lem4  8558  pwsdompw  8635  cfsuc  8688  cflim2  8694  enfin2i  8752  isf34lem4  8808  axdc4lem  8886  zornn0g  8936  uniimadomf  8971  fpwwe2lem8  9063  fpwwe2lem12  9067  fpwwe2lem13  9068  pwfseqlem1  9084  pwfseqlem5  9089  intgru  9240  addclpi  9318  addnidpi  9327  ltsonq  9395  nqpr  9440  reclem3pr  9475  recexsr  9532  supsrlem  9536  infmrclOLD  10594  nnnn0addcl  10901  un0addcl  10904  un0mulcl  10905  nn0nndivcl  10937  nn0ge0div  11006  uzind3  11030  uzind4  11218  zsupss  11254  rpnnen1lem1  11291  rpnnen1lem2  11292  rpnnen1lem3  11293  rpnnen1lem5  11295  ltsubrp  11336  ltaddrp  11337  xrlttr  11440  qbtwnxr  11494  xltnegi  11510  xaddnemnf  11528  xaddnepnf  11529  xaddcom  11532  xnegdi  11535  xsubge0  11548  xrub  11598  fzind2  12023  seqof  12270  expp1  12279  expneg  12280  expcllem  12283  mulexpz  12312  expaddz  12316  expmulz  12318  faclbnd4lem3  12480  faclbnd4  12482  brfi1uzind  12647  swrd00  12765  swrd0  12781  cats1un  12823  reuccats1  12828  cshw0  12887  cshwn  12890  wwlktovfo  13022  shftf  13131  sqrtdiv  13318  leabs  13351  mulcn2  13647  summolem2  13770  fsumrev2  13831  geomulcvg  13920  prodmolem2  13977  zprod  13979  prodsn  14004  prodsnf  14006  bpolydiflem  14095  bpoly2  14098  bpoly3  14099  ruclem6  14275  dvdseq  14340  dvdsfac  14348  gcdcllem1  14461  lcmgcdlem  14559  rpexp1i  14661  hashdvds  14711  iserodd  14773  pcqcl  14794  pcid  14810  ismred  15496  funcpropd  15793  natpropd  15869  lubun  16357  odupos  16369  issubmd  16584  grpinvnzcl  16714  mulgneg  16764  mulgnn0z  16766  symgfixf1  17066  symgsssg  17096  symgfisg  17097  pgpssslw  17254  sylow2alem2  17258  sylow2a  17259  oddvdssubg  17481  gsumzunsnd  17576  gsumunsnfd  17577  gsum2dlem1  17590  gsum2dlem2  17591  ablfac1eu  17694  pgpfac1lem5  17700  gsumdixp  17825  dvdsrcl2  17866  isdrngd  17988  evlslem4  18719  coe1tmmul2  18857  cnsubrg  19016  psgnodpm  19143  gsumcom3  19411  mpt2matmul  19458  cpmidpmat  19884  intcld  20042  neiptopnei  20135  ordtrest2lem  20206  lmss  20301  cmpcovf  20393  cncmp  20394  fincmp  20395  cmpsublem  20401  cmpsub  20402  uncon  20431  1stcfb  20447  2ndcsep  20461  refun0  20517  locfincmp  20528  1stckgenlem  20555  ptbasin  20579  ptbasfi  20583  ptunimpt  20597  ptuniconst  20600  dfac14  20620  ptcnp  20624  xkoptsub  20656  xkococnlem  20661  xkoinjcn  20689  qtopcmplem  20709  qtophmeo  20819  fbfinnfr  20843  isufil2  20910  isfcls  21011  xmetrtri  21357  xmetrtri2  21358  blssioo  21800  divcn  21887  bndth  21973  resscdrg  22312  minveclem3  22358  minveclem3OLD  22370  finiunmbl  22484  opnmbllem  22546  ismbf2d  22584  itg2seq  22687  ellimc2  22819  limcmpt2  22826  limcres  22828  dvlem  22838  dvidlem  22857  dvrec  22896  dveflem  22918  dvlip  22932  coe1mul3  23035  dvtaylp  23312  leibpilem2  23854  leibpi  23855  wilthlem2  23981  basellem3  23996  dvdsflip  24098  dchreq  24173  dchrsum  24184  lgsval3  24229  lgsdir2lem4  24241  2sqlem6  24284  rpvmasumlem  24312  dchrisum0fno1  24336  rpvmasum2  24337  pntrsumbnd2  24392  ostthlem1  24452  colmid  24720  lmiisolem  24825  dfcgra2  24858  axcontlem2  24982  axcontlem7  24987  umgraex  25037  usgraidx2vlem1  25105  nbgraf1olem3  25157  nbgraf1olem5  25159  cusconngra  25390  wlknwwlknfun  25424  wlknwwlkninj  25425  wlknwwlknsur  25426  wlkiswwlkfun  25431  wlkiswwlkinj  25432  wlkiswwlksur  25433  wwlkextfun  25443  wwlkextsur  25445  wlkv0  25474  clwwlkf  25508  grpoidinvlem3  25920  ablo32  26000  ablomuldiv  26003  ablodivdiv  26004  ablodiv32  26006  nvadd12  26228  nvscom  26236  nvsubsub23  26269  dipassr  26473  htthlem  26556  hsn0elch  26887  shscli  26956  nmopun  27653  branmfn  27744  mdslj1i  27958  mdslj2i  27959  atss  27985  chcv1  27994  dmdbr5ati  28061  fcnvgreu  28265  isoun  28272  ordtrest2NEWlem  28724  esumsplit  28870  esumpad2  28873  esumpcvgval  28895  sigaclcu2  28938  ldgenpisyslem1  28981  volmeas  29050  mbfmco2  29083  omsmeas  29151  omsmeasOLD  29152  oddpwdc  29183  eulerpartlemgvv  29205  ballotlemfc0  29321  ballotlemfcc  29322  bnj521  29541  bnj1109  29594  bnj1294  29625  bnj545  29702  bnj605  29714  bnj594  29719  bnj934  29742  bnj953  29746  bnj1137  29800  bnj1174  29808  bnj1388  29838  subfacp1lem4  29902  erdszelem7  29916  erdszelem8  29917  erdsze2lem2  29923  rescon  29965  cvmsdisj  29989  cvmscld  29992  mclsax  30203  climuzcnv  30311  pocnv  30399  trpredmintr  30467  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  31513  relowlssretop  31707  fin2solem  31845  poimirlem4  31858  poimirlem25  31879  poimirlem32  31886  opnmbllem0  31890  mblfinlem3  31893  mbfposadd  31902  itg2addnclem3  31909  bddiblnc  31926  ftc1anclem6  31936  ftc1anc  31939  eqfnun  31962  ac6gf  31973  heibor1lem  32055  isdrngo2  32111  unichnidl  32178  isfldidl  32215  cnf1dd  32240  lkrss2N  32654  elpadd0  33293  ltrnu  33605  tendoex  34461  cdlemm10N  34605  dicfnN  34670  dihmeetlem2N  34786  dihlatat  34824  lcfrlem9  35037  ismrcd1  35459  isnacs3  35471  pellfundglb  35653  jm2.22  35770  jm2.23  35771  isnumbasgrplem1  35880  hbtlem6  35908  rngunsnply  35959  hashgcdlem  35994  phisum  35996  dvgrat  36519  cvgdvgrat  36520  nznngen  36523  uzmptshftfval  36553  iccshift  37450  iooshift  37454  itgperiod  37678  fourierdlem42  37832  fourierdlem42OLD  37833  fourierdlem68  37858  fourierdlem93  37883  elprneb  38424  umgrex  38845  usgridx2vlem1  38928  usgedgppr  38982  usgpredgv  38983  usgpredgvALT  38984  edgssv2ALT  38985  edgssv2  38986  usgedgvadf1lem1  38997  usgedgvadf1ALTlem1  39000  rabsubmgmd  39063  2zlidl  39206  lspsslco  39504