Theorem sylan2b 594

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2b.1	⊢ (𝜑 ↔ 𝜒)
sylan2b.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylan2b	⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan2b.1	. . 3 ⊢ (𝜑 ↔ 𝜒)
2	1	biimpi 216	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2b.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 593	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  syl2anb  598  eupickb  2635  2eu1  2651  2eu1v  2652  eqtr3OLD  2764  elnelne1  3057  elnelne2  3058  morex  3725  psssstr  4109  reuss2  4326  reupick  4329  reximdva0  4355  falseral0  4516  rabsneu  4729  invdisjrab  5130  opabss  5207  triun  5274  triin  5276  poirr  5604  wefrc  5679  xpcan  6196  fnfco  6773  eqfnun  7057  fnressn  7178  fvtp3  7217  fvtp3g  7220  f1mpt  7281  offval  7706  ordsucuniel  7844  onzsl  7867  soex  7943  fiunlem  7966  fiun  7967  f1iun  7968  dfoprab3  8079  poxp  8153  fnwelem  8156  poxp2  8168  suppssr  8220  suppssrg  8221  suppsssn  8226  suppofssd  8228  fprlem2  8326  oeordsuc  8632  oelim2  8633  omsmolem  8695  rexdif1enOLD  9199  ssnnfi  9209  ssfi  9213  ensymfib  9224  domnsymfi  9240  fiint  9366  fiintOLD  9367  unifi  9384  indexfi  9400  iinfi  9457  unwdomg  9624  inf3lem5  9672  rankr1bg  9843  rankr1c  9861  carden2a  10006  dfac8clem  10072  dfac5lem4  10166  dfac5lem4OLD  10168  pwsdompw  10243  cfsuc  10297  cflim2  10303  enfin2i  10361  isf34lem4  10417  axdc4lem  10495  zornn0g  10545  uniimadomf  10585  fpwwe2lem7  10677  fpwwe2lem11  10681  fpwwe2lem12  10682  pwfseqlem1  10698  pwfseqlem5  10703  intgru  10854  addclpi  10932  addnidpi  10941  ltsonq  11009  nqpr  11054  reclem3pr  11089  recexsr  11147  supsrlem  11151  nnnn0addcl  12556  un0addcl  12559  un0mulcl  12560  nn0nndivcl  12598  nn0ge0div  12687  uzind3  12712  uzind4  12948  zsupss  12979  rpnnen1lem2  13019  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  ltsubrp  13071  ltaddrp  13072  xrlttr  13182  qbtwnxr  13242  xltnegi  13258  xaddnemnf  13278  xaddnepnf  13279  xaddcom  13282  xnegdi  13290  xsubge0  13303  xrub  13354  fzne1  13644  fzind2  13824  seqof  14100  expp1  14109  expneg  14110  expcllem  14113  mulexpz  14143  expaddz  14147  expmulz  14149  faclbnd4lem3  14334  faclbnd4  14336  fi1uzind  14546  swrd00  14682  swrd0  14696  cats1un  14759  reuccatpfxs1  14785  cshw0  14832  cshwn  14835  wwlktovfo  14997  shftf  15118  sqrtdiv  15304  leabs  15338  mulcn2  15632  summolem2  15752  fsumrev2  15818  geomulcvg  15912  prodmolem2  15971  zprod  15973  prodsn  15998  prodsnf  16000  fprodle  16032  bpolydiflem  16090  bpoly2  16093  bpoly3  16094  ruclem6  16271  dvdsflip  16354  dvdsfac  16363  gcdcllem1  16536  lcmgcdlem  16643  rpexp1i  16760  hashdvds  16812  hashgcdlem  16825  phisum  16828  iserodd  16873  pcqcl  16894  pcid  16911  ismred  17645  funcpropd  17947  natpropd  18024  odupos  18373  lubun  18560  rabsubmgmd  18717  sgrpidmnd  18752  issubmd  18819  grpinvnzcl  19029  mulgneg  19110  mulgnn0z  19119  symgfixf1  19455  symgsssg  19485  symgfisg  19486  pgpssslw  19632  sylow2alem2  19636  sylow2a  19637  oddvdssubg  19873  gsumzunsnd  19974  gsumunsnfd  19975  gsum2dlem1  19988  gsum2dlem2  19989  gsumcom3  19996  ablfac1eu  20093  pgpfac1lem5  20099  gsumdixp  20316  dvdsrcl2  20366  01eq0ring  20530  isdrngd  20765  isdrngdOLD  20767  cnsubrg  21445  psgnodpm  21606  evlslem4  22100  psdmul  22170  coe1tmmul2  22279  mpomatmul  22452  cpmidpmat  22879  intcld  23048  neiptopnei  23140  ordtrest2lem  23211  lmss  23306  cmpcovf  23399  cncmp  23400  fincmp  23401  cmpsublem  23407  cmpsub  23408  unconn  23437  1stcfb  23453  2ndcsep  23467  refun0  23523  locfincmp  23534  1stckgenlem  23561  ptbasin  23585  ptbasfi  23589  ptunimpt  23603  ptuniconst  23606  dfac14  23626  ptcnp  23630  xkoptsub  23662  xkococnlem  23667  xkoinjcn  23695  qtopcmplem  23715  qtophmeo  23825  fbfinnfr  23849  isufil2  23916  isfcls  24017  xmetrtri  24365  xmetrtri2  24366  blssioo  24816  divcnOLD  24890  divcn  24892  bndth  24990  clmvscom  25123  resscdrg  25392  minveclem3  25463  finiunmbl  25579  opnmbllem  25636  ismbf2d  25675  itg2seq  25777  bddiblnc  25877  ellimc2  25912  limcmpt2  25919  limcres  25921  dvlem  25931  dvidlem  25950  dvrec  25993  dveflem  26017  dvlip  26032  coe1mul3  26138  dvtaylp  26412  leibpilem2  26984  leibpi  26985  wilthlem2  27112  basellem3  27126  dchreq  27302  dchrsum  27313  lgsval3  27359  lgsdir2lem4  27372  2sqlem6  27467  rpvmasumlem  27531  dchrisum0fno1  27555  rpvmasum2  27556  pntrsumbnd2  27611  ostthlem1  27671  nosupno  27748  negsbdaylem  28088  expsp1  28412  colmid  28696  lmiisolem  28804  dfcgra2  28838  axcontlem2  28980  axcontlem7  28985  upgrex  29109  umgredg  29155  umgrpredgv  29157  umgredgne  29162  umgredgnlp  29164  usgredgppr  29213  edgssv2  29215  uspgredg2vlem  29240  usgredg2vlem1  29242  upgrres1  29330  nbuhgr2vtx1edgblem  29368  nbusgrf1o0  29386  hashnbusgrnn0  29393  iscplgredg  29434  uhgrvd00  29552  finsumvtxdg2size  29568  wlkepvtx  29678  wlknewwlksn  29907  wwlksnextfun  29918  wwlksnextsurj  29920  elwwlks2ons3im  29974  wwlks2onsym  29978  clwwlkf  30066  fusgreghash2wspv  30354  numclwwlk5lem  30406  grpoidinvlem3  30525  ablo32  30568  ablomuldiv  30571  ablodivdiv  30572  ablodiv32  30574  nvscom  30648  dipassr  30865  htthlem  30936  hsn0elch  31267  shscli  31336  nmopun  32033  branmfn  32124  mdslj1i  32338  mdslj2i  32339  atss  32365  chcv1  32374  dmdbr5ati  32441  snsssng  32533  ifnebib  32562  fnpreimac  32681  fcnvgreu  32683  isoun  32711  fsuppcurry1  32736  fsuppcurry2  32737  prodpr  32828  prodtp  32829  pmtrprfv2  33108  elrgspnsubrunlem2  33252  nsgmgclem  33439  nsgqusf1olem2  33442  isprmidlc  33475  ssdifidllem  33484  ssdifidlprm  33486  ssmxidllem  33501  qsdrng  33525  1arithufdlem3  33574  ordtrest2NEWlem  33921  esumsplit  34054  esumpad2  34057  esumpcvgval  34079  sigaclcu2  34121  ldgenpisyslem1  34164  volmeas  34232  mbfmco2  34267  omsmeas  34325  oddpwdc  34356  eulerpartlemgvv  34378  ballotlemfc0  34495  ballotlemfcc  34496  prodfzo03  34618  circlemethhgt  34658  bnj1109  34800  bnj1294  34831  bnj545  34909  bnj605  34921  bnj594  34926  bnj934  34949  bnj953  34953  bnj1137  35009  bnj1174  35017  bnj1388  35047  subfacp1lem4  35188  erdszelem7  35202  erdszelem8  35203  erdsze2lem2  35209  resconn  35251  cvmsdisj  35275  cvmscld  35278  satf0op  35382  mclsax  35574  climuzcnv  35676  pocnv  35763  cgrid2  36004  btwncom  36015  btwnswapid2  36019  colinearperm1  36063  colinearperm3  36064  colinearperm2  36065  colinearperm4  36066  lineext  36077  colinbtwnle  36119  broutsideof2  36123  outsideofcom  36129  linecom  36151  linerflx2  36152  lineintmo  36158  fwddifn0  36165  hfext  36184  ntruni  36328  clsint2  36330  neibastop1  36360  weiunlem2  36464  bj-snsetex  36964  relowlssretop  37364  pibt2  37418  fin2solem  37613  lindsadd  37620  matunitlindflem1  37623  poimirlem4  37631  poimirlem25  37652  poimirlem32  37659  opnmbllem0  37663  mblfinlem3  37666  mbfposadd  37674  itg2addnclem3  37680  ftc1anclem6  37705  ftc1anc  37708  ac6gf  37739  heibor1lem  37816  isdrngo2  37965  unichnidl  38038  isfldidl  38075  cnf1dd  38097  membpartlem19  38812  lkrss2N  39170  elpadd0  39811  ltrnu  40123  tendoex  40977  cdlemm10N  41120  dicfnN  41185  dihmeetlem2N  41301  dihlatat  41339  lcfrlem9  41552  uzindd  41978  sticksstones1  42147  metakunt12  42217  ofun  42277  nn0addcom  42480  nn0mulcom  42484  zmulcomlem  42485  fsuppind  42600  prjspner1  42636  infdesc  42653  ismrcd1  42709  isnacs3  42721  pellfundglb  42896  jm2.22  43007  jm2.23  43008  isnumbasgrplem1  43113  hbtlem6  43141  rngunsnply  43181  ordsssucim  43415  mnringmulrcld  44247  dvgrat  44331  cvgdvgrat  44332  nznngen  44335  uzmptshftfval  44365  wfac8prim  45019  rnmptlb  45250  rnmptbddlem  45251  rnmptbd2lem  45255  iccshift  45531  iooshift  45535  liminflbuz2  45830  xlimbr  45842  itgperiod  45996  fourierdlem42  46164  fourierdlem68  46189  fourierdlem93  46214  smfpimne2  46855  elprneb  47041  dfatcolem  47267  ichim  47444  ichnfb  47452  prproropf1olem1  47490  prproropf1olem3  47492  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  2zlidl  48156  lspsslco  48354  isthincd2  49086  fullthinc  49099