Theorem sylan2b 475

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  syl2anb  479  bianir  967  eupickb  2360  bm1.1OLD  2441  eqtr3  2485  elnelne1  2804  elnelne2  2805  morex  3283  psssstr  3606  reuss2  3785  reupick  3789  reximdva0  3805  rabsneu  4107  opabss  4518  triun  4563  poirr  4820  wefrc  4882  xpcan  5450  fnfco  5756  suppssrOLD  6022  fnressn  6084  fvtp3  6121  fvtp3g  6124  f1mpt  6170  offval  6546  ordsucuniel  6658  onzsl  6680  soex  6742  fun11iun  6759  dfoprab3  6855  1stconst  6887  2ndconst  6888  poxp  6911  fnwelem  6914  suppssr  6949  suppsssn  6953  oeordsuc  7261  oelim2  7262  omsmolem  7320  fisucdomOLD  7742  ssnnfi  7758  fiint  7815  unifi  7827  indexfi  7846  iinfi  7895  unwdomg  8028  inf3lem5  8066  rankr1bg  8238  rankr1c  8256  carden2a  8364  dfac8clem  8430  dfac5lem4  8524  pwsdompw  8601  cfsuc  8654  cflim2  8660  enfin2i  8718  isf34lem4  8774  axdc4lem  8852  zornn0g  8902  uniimadomf  8937  fpwwe2lem8  9032  fpwwe2lem12  9036  fpwwe2lem13  9037  pwfseqlem1  9053  pwfseqlem5  9058  intgru  9209  addclpi  9287  addnidpi  9296  ltsonq  9364  nqpr  9409  reclem3pr  9444  recexsr  9501  supsrlem  9505  infmrcl  10542  nnnn0addcl  10847  un0addcl  10850  un0mulcl  10851  nn0nndivcl  10884  nn0ge0div  10953  uzind3  10977  uzind3OLD  10979  uzind4  11164  zsupss  11196  rpnnen1lem1  11233  rpnnen1lem2  11234  rpnnen1lem3  11235  rpnnen1lem5  11237  ltsubrp  11276  ltaddrp  11277  xrlttr  11371  qbtwnxr  11424  xltnegi  11440  xaddnemnf  11458  xaddnepnf  11459  xaddcom  11462  xnegdi  11465  xsubge0  11478  xrub  11528  fzind2  11927  seqof  12167  expp1  12176  expneg  12177  expcllem  12180  mulexpz  12209  expaddz  12213  expmulz  12215  faclbnd4lem3  12376  faclbnd4  12378  brfi1uzind  12536  swrd00  12654  swrd0  12670  cats1un  12713  reuccats1  12718  cshw0  12777  cshwn  12780  wwlktovfo  12908  shftf  12924  sqrtdiv  13111  leabs  13144  mulcn2  13430  summolem2  13550  fsumrev2  13609  geomulcvg  13697  prodmolem2  13754  zprod  13756  prodsn  13779  ruclem6  13980  dvdseq  14045  dvdsfac  14053  gcdcllem1  14161  rpexp1i  14274  hashdvds  14317  iserodd  14371  pcqcl  14392  pcid  14408  ismred  15019  funcpropd  15316  natpropd  15392  lubun  15880  odupos  15892  issubmd  16107  grpinvnzcl  16237  mulgneg  16287  mulgnn0z  16289  symgfixf1  16589  symgsssg  16619  symgfisg  16620  pgpssslw  16761  sylow2alem2  16765  sylow2a  16766  oddvdssubg  16988  gsumzunsnd  17109  gsumunsnfd  17110  gsum2dlem1  17124  gsum2dlem2  17125  gsum2dOLD  17127  ablfac1eu  17251  pgpfac1lem5  17257  gsumdixpOLD  17384  gsumdixp  17385  dvdsrcl2  17426  isdrngd  17548  evlslem4OLD  18300  evlslem4  18301  coe1tmmul2  18444  cnsubrg  18605  psgnodpm  18751  gsumcom3  19028  mpt2matmul  19075  cpmidpmat  19501  intcld  19668  neiptopnei  19760  ordtrest2lem  19831  lmss  19926  cmpcovf  20018  cncmp  20019  fincmp  20020  cmpsublem  20026  cmpsub  20027  uncon  20056  1stcfb  20072  2ndcsep  20086  refun0  20142  locfincmp  20153  1stckgenlem  20180  ptbasin  20204  ptbasfi  20208  ptunimpt  20222  ptuniconst  20225  dfac14  20245  ptcnp  20249  xkoptsub  20281  xkococnlem  20286  xkoinjcn  20314  qtopcmplem  20334  qtophmeo  20444  fbfinnfr  20468  isufil2  20535  isfcls  20636  xmetrtri  20984  xmetrtri2  20985  blssioo  21426  divcn  21498  bndth  21584  resscdrg  21924  minveclem3  21970  finiunmbl  22080  opnmbllem  22136  ismbf2d  22174  itg2seq  22275  ellimc2  22407  limcmpt2  22414  limcres  22416  dvlem  22426  dvidlem  22445  dvrec  22484  dveflem  22506  dvlip  22520  coe1mul3  22626  dvtaylp  22891  leibpilem2  23398  leibpi  23399  wilthlem2  23469  basellem3  23482  dvdsflip  23584  dchreq  23659  dchrsum  23670  lgsval3  23715  lgsdir2lem4  23727  2sqlem6  23770  rpvmasumlem  23798  dchrisum0fno1  23822  rpvmasum2  23823  pntrsumbnd2  23878  ostthlem1  23938  colmid  24191  lmiisolem  24287  axcontlem2  24395  axcontlem7  24400  umgraex  24450  usgraidx2vlem1  24518  nbgraf1olem3  24570  nbgraf1olem5  24572  cusconngra  24803  wlknwwlknfun  24837  wlknwwlkninj  24838  wlknwwlknsur  24839  wlkiswwlkfun  24844  wlkiswwlkinj  24845  wlkiswwlksur  24846  wwlkextfun  24856  wwlkextsur  24858  wlkv0  24887  clwwlkf  24921  grpoidinvlem3  25335  ablo32  25415  ablomuldiv  25418  ablodivdiv  25419  ablodiv32  25421  nvadd12  25643  nvscom  25651  nvsubsub23  25684  dipassr  25888  htthlem  25961  hsn0elch  26293  shscli  26362  nmopun  27060  branmfn  27151  mdslj1i  27365  mdslj2i  27366  atss  27392  chcv1  27401  dmdbr5ati  27468  fcnvgreu  27668  isoun  27675  ordtrest2NEWlem  28065  esumsplit  28227  esumpcvgval  28250  sigaclcu2  28293  volmeas  28376  mbfmco2  28409  oddpwdc  28490  eulerpartlemgvv  28512  ballotlemfc0  28628  ballotlemfcc  28629  subfacp1lem4  28824  erdszelem7  28838  erdszelem8  28839  erdsze2lem2  28845  rescon  28888  cvmsdisj  28912  cvmscld  28915  mclsax  29126  climuzcnv  29234  pocnv  29411  trpredmintr  29531  cgrid2  29858  btwncom  29869  btwnswapid2  29873  colinearperm1  29917  colinearperm3  29918  colinearperm2  29919  colinearperm4  29920  lineext  29931  colinbtwnle  29973  broutsideof2  29977  outsideofcom  29983  linecom  30005  linerflx2  30006  lineintmo  30012  bpolydiflem  30021  bpoly2  30024  bpoly3  30025  hfext  30045  fin2solem  30244  opnmbllem0  30255  mblfinlem3  30258  mbfposadd  30267  itg2addnclem3  30273  bddiblnc  30290  ftc1anclem6  30300  ftc1anc  30303  ntruni  30350  clsint2  30352  neibastop1  30382  eqfnun  30417  ac6gf  30428  heibor1lem  30510  isdrngo2  30566  unichnidl  30633  isfldidl  30670  cnf1dd  30695  ismrcd1  30835  isnacs3  30847  pellfundglb  31025  jm2.22  31141  jm2.23  31142  isnumbasgrplem1  31254  hbtlem6  31282  rngunsnply  31326  hashgcdlem  31361  phisum  31363  dvgrat  31397  cvgdvgrat  31398  lcmgcdlem  31416  nznngen  31425  uzmptshftfval  31455  iccshift  31761  iooshift  31765  prodsnf  31790  itgperiod  31983  fourierdlem42  32134  fourierdlem68  32160  fourierdlem93  32185  usgedgppr  32660  usgpredgv  32661  usgpredgvALT  32662  edgssv2ALT  32663  edgssv2  32664  usgedgvadf1lem1  32675  usgedgvadf1ALTlem1  32678  rabsubmgmd  32741  2zlidl  32884  lspsslco  33182  bnj521  33935  bnj1109  33988  bnj1294  34019  bnj545  34096  bnj605  34108  bnj594  34113  bnj934  34136  bnj953  34140  bnj1137  34194  bnj1174  34202  bnj1388  34232  bj-snsetex  34664  lkrss2N  35037  elpadd0  35676  ltrnu  35988  tendoex  36844  cdlemm10N  36988  dicfnN  37053  dihmeetlem2N  37169  dihlatat  37207  lcfrlem9  37420