Theorem sylan2b 472

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 471	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  476  bianir  951  eupickb  2340  bm1.1  2418  eqtr3  2452  morex  3132  psssstr  3450  reuss2  3618  reupick  3622  reximdva0  3636  rabsneu  3938  opabss  4341  triun  4386  poirr  4639  wefrc  4701  xpcan  5262  fnfco  5565  suppssrOLD  5825  eldmrexrnb  5838  fnressn  5881  fvtp3  5914  fvtp3g  5917  f1mpt  5961  offval  6316  ordsucuniel  6424  onzsl  6446  soex  6510  fun11iun  6526  dfoprab3  6619  1stconst  6650  2ndconst  6651  poxp  6673  fnwelem  6676  suppssr  6709  suppsssn  6713  oeordsuc  7021  oelim2  7022  omsmolem  7080  fisucdomOLD  7504  ssnnfi  7520  fiint  7576  unifi  7588  indexfi  7607  iinfi  7655  unwdomg  7787  inf3lem5  7826  rankr1bg  7998  rankr1c  8016  carden2a  8124  dfac8clem  8190  dfac5lem4  8284  pwsdompw  8361  cfsuc  8414  cflim2  8420  enfin2i  8478  isf34lem4  8534  axdc4lem  8612  zornn0g  8662  uniimadomf  8697  fpwwe2lem8  8791  fpwwe2lem12  8795  fpwwe2lem13  8796  pwfseqlem1  8812  pwfseqlem5  8817  intgru  8968  addclpi  9048  addnidpi  9057  ltsonq  9125  nqpr  9170  reclem3pr  9205  recexsr  9261  supsrlem  9265  infmrcl  10296  nnnn0addcl  10597  un0addcl  10600  un0mulcl  10601  nn0nndivcl  10632  nn0ge0div  10698  uzind3  10722  uzind3OLD  10724  uzind4  10899  zsupss  10931  rpnnen1lem1  10966  rpnnen1lem2  10967  rpnnen1lem3  10968  rpnnen1lem5  10970  ltsubrp  11009  ltaddrp  11010  xrlttr  11104  qbtwnxr  11157  xltnegi  11173  xaddnemnf  11191  xaddnepnf  11192  xaddcom  11195  xnegdi  11198  xsubge0  11211  xrub  11261  fzind2  11620  seqof  11846  expp1  11855  expneg  11856  expcllem  11859  mulexpz  11887  expaddz  11891  expmulz  11893  faclbnd4lem3  12054  faclbnd4  12056  brfi1uzind  12202  swrd00  12297  swrd0  12310  cats1un  12353  cshw0  12414  cshwn  12417  shftf  12551  sqrdiv  12738  leabs  12771  mulcn2  13056  summolem2  13176  fsumrev2  13231  geomulcvg  13318  ruclem6  13499  dvdseq  13562  dvdsfac  13570  gcdcllem1  13677  rpexp1i  13789  hashdvds  13832  iserodd  13884  pcqcl  13905  pcid  13921  ismred  14522  funcpropd  14792  natpropd  14868  lubun  15275  odupos  15287  issubmd  15458  grpinvnzcl  15577  mulgneg  15624  mulgnn0z  15626  symgfixf1  15922  symgsssg  15952  symgfisg  15953  pgpssslw  16092  sylow2alem2  16096  sylow2a  16097  oddvdssubg  16316  gsumunsnd  16426  gsum2dlem1  16434  gsum2dlem2  16435  gsum2dOLD  16437  ablfac1eu  16547  pgpfac1lem5  16553  gsumdixpOLD  16634  gsumdixp  16635  dvdsrcl2  16675  isdrngd  16780  evlslem4OLD  17517  evlslem4  17518  coe1tmmul2  17626  cnsubrg  17716  psgnodpm  17859  gsumcom3  18140  intcld  18485  neiptopnei  18577  ordtrest2lem  18648  lmss  18743  cmpcovf  18835  cncmp  18836  fincmp  18837  cmpsublem  18843  cmpsub  18844  uncon  18874  1stcfb  18890  2ndcsep  18904  1stckgenlem  18967  ptbasin  18991  ptbasfi  18995  ptunimpt  19009  ptuniconst  19012  dfac14  19032  ptcnp  19036  xkoptsub  19068  xkococnlem  19073  xkoinjcn  19101  qtopcmplem  19121  qtophmeo  19231  fbfinnfr  19255  isfcls  19423  psmettri2  19726  xmetrtri  19771  xmetrtri2  19772  blssioo  20213  divcn  20285  bndth  20371  resscdrg  20711  minveclem3  20757  finiunmbl  20866  opnmbllem  20922  ismbf2d  20960  itg2seq  21061  ellimc2  21193  limcmpt2  21200  limcres  21202  dvlem  21212  dvidlem  21231  dvrec  21270  dveflem  21292  dvlip  21306  coe1mul3  21455  dvtaylp  21719  leibpilem2  22220  leibpi  22221  wilthlem2  22291  basellem3  22304  dvdsflip  22406  dchreq  22481  dchrsum  22492  lgsval3  22537  lgsdir2lem4  22549  2sqlem6  22592  rpvmasumlem  22620  dchrisum0fno1  22644  rpvmasum2  22645  pntrsumbnd2  22700  ostthlem1  22760  axcontlem2  23033  axcontlem7  23038  umgraex  23079  usgraidx2vlem1  23131  nbgraf1olem3  23174  nbgraf1olem5  23176  cusconngra  23384  grpoidinvlem3  23515  ablo32  23595  ablomuldiv  23598  ablodivdiv  23599  ablodiv32  23601  nvadd12  23823  nvscom  23831  nvsubsub23  23864  dipassr  24068  htthlem  24141  hsn0elch  24473  shscli  24542  nmopun  25240  branmfn  25331  mdslj1i  25545  mdslj2i  25546  atss  25572  chcv1  25581  dmdbr5ati  25648  fcnvgreu  25814  isoun  25820  gsumunsnf  26096  ordtrest2NEWlem  26205  esumsplit  26359  esumpcvgval  26380  sigaclcu2  26416  volmeas  26500  mbfmco2  26533  oddpwdc  26584  eulerpartlemgvv  26606  ballotlemfc0  26722  ballotlemfcc  26723  subfacp1lem4  26918  erdszelem7  26932  erdszelem8  26933  erdsze2lem2  26939  rescon  26982  cvmsdisj  27006  cvmscld  27009  climuzcnv  27162  prodmolem2  27294  zprod  27296  prodsn  27319  pocnv  27420  trpredmintr  27541  cgrid2  27880  btwncom  27891  btwnswapid2  27895  colinearperm1  27939  colinearperm3  27940  colinearperm2  27941  colinearperm4  27942  lineext  27953  colinbtwnle  27995  broutsideof2  27999  outsideofcom  28005  linecom  28027  linerflx2  28028  lineintmo  28034  bpolydiflem  28043  bpoly2  28046  bpoly3  28047  hfext  28067  fin2solem  28256  opnmbllem0  28268  mblfinlem3  28271  mbfposadd  28280  itg2addnclem3  28286  bddiblnc  28303  ftc1anclem6  28313  ftc1anc  28316  ntruni  28363  clsint2  28365  locfincmp  28417  neibastop1  28421  eqfnun  28456  ac6gf  28467  heibor1lem  28549  isdrngo2  28605  unichnidl  28672  isfldidl  28709  ismrcd1  28876  isnacs3  28888  pellfundglb  29068  jm2.22  29186  jm2.23  29187  isnumbasgrplem1  29299  hbtlem6  29327  rngunsnply  29372  hashgcdlem  29407  phisum  29409  afv0nbfvbi  29900  wwlktovfo  30096  reuccats1  30104  wlkv0  30134  wlknwwlknfun  30185  wlknwwlkninj  30186  wlknwwlknsur  30187  wlkiswwlkfun  30192  wlkiswwlkinj  30193  wlkiswwlksur  30194  wwlkextfun  30204  wwlkextsur  30206  clwwlkf  30299  lspsslco  30677  bnj521  31427  bnj1109  31479  bnj1294  31510  bnj545  31587  bnj605  31599  bnj594  31604  bnj934  31627  bnj953  31631  bnj1137  31685  bnj1174  31693  bnj1388  31723  bj-snsetex  32036  lkrss2N  32384  elpadd0  33023  ltrnu  33335  tendoex  34189  cdlemm10N  34333  dicfnN  34398  dihmeetlem2N  34514  dihlatat  34552  lcfrlem9  34765