Theorem sylan2b 492

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  syl2anb  496  eupickb  2538  eqtr3  2643  elnelne1  2907  elnelne2  2908  morex  3390  psssstr  3713  reuss2  3907  reupick  3911  reximdva0  3933  falseral0  4081  rabsneu  4264  opabss  4714  triun  4766  poirr  5046  wefrc  5108  xpcan  5570  fnfco  6069  fnressn  6425  fvtp3  6462  fvtp3g  6465  f1mpt  6518  offval  6904  ordsucuniel  7024  onzsl  7046  soex  7109  fun11iun  7126  dfoprab3  7224  1stconst  7265  2ndconst  7266  poxp  7289  fnwelem  7292  suppssr  7326  suppsssn  7330  oeordsuc  7674  oelim2  7675  omsmolem  7733  ssnnfi  8179  fiint  8237  unifi  8255  indexfi  8274  iinfi  8323  unwdomg  8489  inf3lem5  8529  rankr1bg  8666  rankr1c  8684  carden2a  8792  dfac8clem  8855  dfac5lem4  8949  pwsdompw  9026  cfsuc  9079  cflim2  9085  enfin2i  9143  isf34lem4  9199  axdc4lem  9277  zornn0g  9327  uniimadomf  9367  fpwwe2lem8  9459  fpwwe2lem12  9463  fpwwe2lem13  9464  pwfseqlem1  9480  pwfseqlem5  9485  intgru  9636  addclpi  9714  addnidpi  9723  ltsonq  9791  nqpr  9836  reclem3pr  9871  recexsr  9928  supsrlem  9932  nnnn0addcl  11323  un0addcl  11326  un0mulcl  11327  nn0nndivcl  11362  nn0ge0div  11446  uzind3  11471  uzind4  11746  zsupss  11777  rpnnen1lem2  11814  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  ltsubrp  11866  ltaddrp  11867  xrlttr  11973  qbtwnxr  12031  xltnegi  12047  xaddnemnf  12067  xaddnepnf  12068  xaddcom  12071  xnegdi  12078  xsubge0  12091  xrub  12142  fzind2  12586  seqof  12858  expp1  12867  expneg  12868  expcllem  12871  mulexpz  12900  expaddz  12904  expmulz  12906  faclbnd4lem3  13082  faclbnd4  13084  fi1uzind  13279  fi1uzindOLD  13285  swrd00  13418  swrd0  13434  cats1un  13475  reuccats1  13480  cshw0  13540  cshwn  13543  wwlktovfo  13701  shftf  13819  sqrtdiv  14006  leabs  14039  mulcn2  14326  summolem2  14447  fsumrev2  14514  geomulcvg  14607  prodmolem2  14665  zprod  14667  prodsn  14692  prodsnf  14694  bpolydiflem  14785  bpoly2  14788  bpoly3  14789  ruclem6  14964  dvdsflip  15039  dvdsfac  15048  gcdcllem1  15221  lcmgcdlem  15319  rpexp1i  15433  hashdvds  15480  hashgcdlem  15493  phisum  15495  iserodd  15540  pcqcl  15561  pcid  15577  ismred  16262  funcpropd  16560  natpropd  16636  lubun  17123  odupos  17135  issubmd  17349  grpinvnzcl  17487  mulgneg  17560  mulgnn0z  17567  symgfixf1  17857  symgsssg  17887  symgfisg  17888  pgpssslw  18029  sylow2alem2  18033  sylow2a  18034  oddvdssubg  18258  gsumzunsnd  18355  gsumunsnfd  18356  gsum2dlem1  18369  gsum2dlem2  18370  ablfac1eu  18472  pgpfac1lem5  18478  gsumdixp  18609  dvdsrcl2  18650  isdrngd  18772  evlslem4  19508  coe1tmmul2  19646  cnsubrg  19806  psgnodpm  19934  gsumcom3  20205  mpt2matmul  20252  cpmidpmat  20678  intcld  20844  neiptopnei  20936  ordtrest2lem  21007  lmss  21102  cmpcovf  21194  cncmp  21195  fincmp  21196  cmpsublem  21202  cmpsub  21203  unconn  21232  1stcfb  21248  2ndcsep  21262  refun0  21318  locfincmp  21329  1stckgenlem  21356  ptbasin  21380  ptbasfi  21384  ptunimpt  21398  ptuniconst  21401  dfac14  21421  ptcnp  21425  xkoptsub  21457  xkococnlem  21462  xkoinjcn  21490  qtopcmplem  21510  qtophmeo  21620  fbfinnfr  21645  isufil2  21712  isfcls  21813  xmetrtri  22160  xmetrtri2  22161  blssioo  22598  divcn  22671  bndth  22757  clmvscom  22890  resscdrg  23154  minveclem3  23200  finiunmbl  23312  opnmbllem  23369  ismbf2d  23408  itg2seq  23509  ellimc2  23641  limcmpt2  23648  limcres  23650  dvlem  23660  dvidlem  23679  dvrec  23718  dveflem  23742  dvlip  23756  coe1mul3  23859  dvtaylp  24124  leibpilem2  24668  leibpi  24669  wilthlem2  24795  basellem3  24809  dchreq  24983  dchrsum  24994  lgsval3  25040  lgsdir2lem4  25053  2sqlem6  25148  rpvmasumlem  25176  dchrisum0fno1  25200  rpvmasum2  25201  pntrsumbnd2  25256  ostthlem1  25316  colmid  25583  lmiisolem  25688  dfcgra2  25721  axcontlem2  25845  axcontlem7  25850  upgrex  25987  umgredg  26033  umgrpredgv  26035  umgredgne  26040  umgredgnlp  26042  usgredgppr  26088  edgssv2  26090  uspgredg2vlem  26115  usgredg2vlem1  26117  upgrres1  26205  nbuhgr2vtx1edgblem  26247  nbusgrf1o0  26271  hashnbusgrnn0  26278  iscplgredg  26313  uhgrvd00  26430  finsumvtxdg2size  26446  wlkepvtx  26556  wlknewwlksn  26773  wlknwwlksnfun  26774  wlknwwlksninj  26775  wlknwwlksnsur  26776  wlkwwlkfun  26781  wlkwwlkinj  26782  wlkwwlksur  26783  wwlksnextfun  26793  wwlksnextsur  26795  elwwlks2ons3  26848  wwlks2onsym  26851  clwwlksf  26915  fusgreghash2wspv  27199  grpoidinvlem3  27360  ablo32  27403  ablomuldiv  27406  ablodivdiv  27407  ablodiv32  27409  nvscom  27484  dipassr  27701  htthlem  27774  hsn0elch  28105  shscli  28176  nmopun  28873  branmfn  28964  mdslj1i  29178  mdslj2i  29179  atss  29205  chcv1  29214  dmdbr5ati  29281  fcnvgreu  29472  isoun  29479  prodpr  29572  prodtp  29573  ordtrest2NEWlem  29968  esumsplit  30115  esumpad2  30118  esumpcvgval  30140  sigaclcu2  30183  ldgenpisyslem1  30226  volmeas  30294  mbfmco2  30327  omsmeas  30385  oddpwdc  30416  eulerpartlemgvv  30438  ballotlemfc0  30554  ballotlemfcc  30555  prodfzo03  30681  circlemethhgt  30721  bnj521  30805  bnj1109  30857  bnj1294  30888  bnj545  30965  bnj605  30977  bnj594  30982  bnj934  31005  bnj953  31009  bnj1137  31063  bnj1174  31071  bnj1388  31101  subfacp1lem4  31165  erdszelem7  31179  erdszelem8  31180  erdsze2lem2  31186  resconn  31228  cvmsdisj  31252  cvmscld  31255  mclsax  31466  climuzcnv  31565  pocnv  31653  trpredmintr  31731  nosupno  31849  cgrid2  32110  btwncom  32121  btwnswapid2  32125  colinearperm1  32169  colinearperm3  32170  colinearperm2  32171  colinearperm4  32172  lineext  32183  colinbtwnle  32225  broutsideof2  32229  outsideofcom  32235  linecom  32257  linerflx2  32258  lineintmo  32264  fwddifn0  32271  hfext  32290  ntruni  32322  clsint2  32324  neibastop1  32354  bj-snsetex  32951  relowlssretop  33211  fin2solem  33395  matunitlindflem1  33405  poimirlem4  33413  poimirlem25  33434  poimirlem32  33441  opnmbllem0  33445  mblfinlem3  33448  mbfposadd  33457  itg2addnclem3  33463  bddiblnc  33480  ftc1anclem6  33490  ftc1anc  33493  eqfnun  33516  ac6gf  33527  heibor1lem  33608  isdrngo2  33757  unichnidl  33830  isfldidl  33867  cnf1dd  33892  lkrss2N  34456  elpadd0  35095  ltrnu  35407  tendoex  36263  cdlemm10N  36407  dicfnN  36472  dihmeetlem2N  36588  dihlatat  36626  lcfrlem9  36839  ismrcd1  37261  isnacs3  37273  pellfundglb  37449  jm2.22  37562  jm2.23  37563  isnumbasgrplem1  37671  hbtlem6  37699  rngunsnply  37743  dvgrat  38511  cvgdvgrat  38512  nznngen  38515  uzmptshftfval  38545  iccshift  39744  iooshift  39748  xlimbr  40053  itgperiod  40197  fourierdlem42  40366  fourierdlem68  40391  fourierdlem93  40416  elprneb  41296  rabsubmgmd  41791  2zlidl  41934  lspsslco  42226  setrec2lem2  42441