Theorem sylan2b 605

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 219	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2b.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 604	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  syl2anb  609  eupickb  2669  2eu1  2684  2eu1v  2685  elnelne1  3081  elnelne2  3082  morex  3691  psssstr  4072  reuss2  4287  reupick  4290  reximdva0  4317  falseral0OLD  4478  rabsneu  4697  invdisjrab  5097  opabss  5176  triun  5234  triin  5236  poirr  5579  wefrc  5653  xpcan  6173  fnfco  6741  eqfnun  7030  fnressn  7153  fvtp3  7193  fvtp3g  7196  f1mpt  7257  offval  7681  ordsucuniel  7816  onzsl  7838  soex  7914  fiunlem  7935  fiun  7936  f1iun  7937  dfoprab3  8047  poxp  8120  fnwelem  8123  poxp2  8135  suppssr  8187  suppssrg  8188  suppsssn  8193  suppofssd  8195  fprlem2  8294  oeordsuc  8576  oelim2  8577  omsmolem  8639  ssnnfi  9150  ssfi  9153  ensymfib  9164  domnsymfi  9180  fiint  9282  unifi  9297  indexfi  9313  iinfi  9373  unwdomg  9542  inf3lem5  9597  rankr1bg  9771  rankr1c  9789  carden2a  9948  dfac8clem  10012  dfac5lem4  10106  pwsdompw  10182  cfsuc  10237  cflim2  10243  enfin2i  10301  isf34lem4  10357  axdc4lem  10435  zornn0g  10485  uniimadomf  10525  fpwwe2lem7  10618  fpwwe2lem11  10622  fpwwe2lem12  10623  pwfseqlem1  10639  pwfseqlem5  10644  intgru  10795  addclpi  10873  addnidpi  10882  ltsonq  10950  nqpr  10995  reclem3pr  11030  recexsr  11088  supsrlem  11092  nnnn0addcl  12530  un0addcl  12533  un0mulcl  12534  nn0nndivcl  12572  nn0ge0div  12661  uzind3  12686  uzind4  12926  zsupss  12957  rpnnen1lem2  12997  rpnnen1lem1  12998  rpnnen1lem3  12999  rpnnen1lem5  13001  ltsubrp  13050  ltaddrp  13051  xrlttr  13161  qbtwnxr  13222  xltnegi  13238  xaddnemnf  13258  xaddnepnf  13259  xaddcom  13262  xnegdi  13270  xsubge0  13283  xrub  13334  fzne1  13628  fzind2  13813  seqof  14091  expp1  14100  expneg  14101  expcllem  14104  mulexpz  14134  expaddz  14138  expmulz  14140  faclbnd4lem3  14327  faclbnd4  14329  fi1uzind  14540  swrd00  14678  swrd0  14692  cats1un  14754  reuccatpfxs1  14780  cshw0  14827  cshwn  14830  wwlktovfo  14991  shftf  15112  sqrtdiv  15312  leabs  15346  mulcn2  15643  summolem2  15763  fsumrev2  15829  geomulcvg  15926  prodmolem2  15985  zprod  15987  prodsn  16012  prodsnf  16014  fprodle  16046  bpolydiflem  16104  bpoly2  16107  bpoly3  16108  ruclem6  16287  dvdsflip  16371  dvdsfac  16380  gcdcllem1  16553  lcmgcdlem  16660  rpexp1i  16778  hashdvds  16830  hashgcdlem  16843  phisum  16846  iserodd  16891  pcqcl  16912  pcid  16929  ismred  17650  funcpropd  17955  natpropd  18032  odupos  18378  lubun  18567  rabsubmgmd  18758  sgrpidmnd  18793  issubmd  18860  grpinvnzcl  19073  mulgneg  19154  mulgnn0z  19163  symgfixf1  19503  symgsssg  19533  symgfisg  19534  pgpssslw  19680  sylow2alem2  19684  sylow2a  19685  oddvdssubg  19921  gsumzunsnd  20022  gsumunsnfd  20023  gsum2dlem1  20036  gsum2dlem2  20037  gsumcom3  20044  ablfac1eu  20141  pgpfac1lem5  20147  gsumdixp  20396  dvdsrcl2  20444  01eq0ring  20610  isdrngd  20843  isdrngdOLD  20845  unichnlidl  21336  isprmidlc  21439  ssdifidllem  21449  ssdifidlprm  21451  cnsubrg  21542  psgnodpm  21703  evlslem4  22192  psdmul  22294  coe1tmmul2  22402  mpomatmul  22568  cpmidpmat  22995  intcld  23162  neiptopnei  23254  ordtrest2lem  23325  lmss  23420  cmpcovf  23513  cncmp  23514  fincmp  23515  cmpsublem  23521  cmpsub  23522  unconn  23551  1stcfb  23567  2ndcsep  23581  refun0  23637  locfincmp  23648  1stckgenlem  23675  ptbasin  23699  ptbasfi  23703  ptunimpt  23717  ptuniconst  23720  dfac14  23740  ptcnp  23744  xkoptsub  23776  xkococnlem  23781  xkoinjcn  23809  qtopcmplem  23829  qtophmeo  23939  fbfinnfr  23963  isufil2  24030  isfcls  24131  xmetrtri  24477  xmetrtri2  24478  blssioo  24917  divcn  24992  bndth  25082  clmvscom  25214  resscdrg  25482  minveclem3  25553  finiunmbl  25668  opnmbllem  25725  ismbf2d  25764  itg2seq  25866  bddiblnc  25966  ellimc2  26001  limcmpt2  26008  limcres  26010  dvlem  26020  dvidlem  26039  dvrec  26079  dveflem  26103  dvlip  26117  coe1mul3  26221  dvtaylp  26495  leibpilem2  27068  leibpi  27069  wilthlem2  27195  basellem3  27209  dchreq  27384  dchrsum  27395  lgsval3  27441  lgsdir2lem4  27454  2sqlem6  27549  rpvmasumlem  27613  dchrisum0fno1  27637  rpvmasum2  27638  pntrsumbnd2  27693  ostthlem1  27753  nosupno  27829  negbdaylem  28211  expsp1  28584  colmid  28923  plngrotlem2  29024  lmiisolem  29059  dfcgra2  29094  prlngmolem2  29152  axcontlem2  29252  axcontlem7  29257  upgrex  29379  umgredg  29425  umgrpredgv  29427  umgredgne  29432  umgredgnlp  29434  usgredgppr  29483  edgssv2  29485  uspgredg2vlem  29510  usgredg2vlem1  29512  upgrres1  29600  nbuhgr2vtx1edgblem  29638  nbusgrf1o0  29656  hashnbusgrnn0  29663  iscplgredg  29704  uhgrvd00  29821  finsumvtxdg2size  29837  wlkepvtx  29945  wlknewwlksn  30173  wwlksnextfun  30184  wwlksnextsurj  30186  elwwlks2ons3im  30240  wwlks2onsym  30246  clwwlkf  30335  fusgreghash2wspv  30623  numclwwlk5lem  30675  grpoidinvlem3  30795  ablo32  30838  ablomuldiv  30841  ablodivdiv  30842  ablodiv32  30844  nvscom  30918  dipassr  31135  htthlem  31206  hsn0elch  31537  shscli  31606  nmopun  32303  branmfn  32394  mdslj1i  32608  mdslj2i  32609  atss  32635  chcv1  32644  dmdbr5ati  32711  snsssng  32797  ifnebib  32832  fnpreimac  32952  fcnvgreu  32954  isoun  32984  fsuppcurry1  33006  fsuppcurry2  33007  prodpr  33107  prodtp  33108  pmtrprfv2  33345  elrgspnsubrunlem2  33505  nsgmgclem  33660  nsgqusf1olem2  33663  ssmxidllem  33697  qsdrng  33720  1arithufdlem3  33777  ordtrest2NEWlem  34253  esumsplit  34384  esumpad2  34387  esumpcvgval  34409  sigaclcu2  34451  ldgenpisyslem1  34494  volmeas  34562  mbfmco2  34596  omsmeas  34654  oddpwdc  34685  eulerpartlemgvv  34707  ballotlemfc0  34824  ballotlemfcc  34825  prodfzo03  34931  circlemethhgt  34971  bnj1109  35116  bnj1294  35146  bnj545  35224  bnj605  35236  bnj594  35241  bnj934  35264  bnj953  35268  bnj1137  35324  bnj1174  35332  bnj1388  35362  vonf1oonfo  35494  subfacp1lem4  35570  erdszelem7  35584  erdszelem8  35585  erdsze2lem2  35591  resconn  35633  cvmsdisj  35657  cvmscld  35660  satf0op  35764  mclsax  35956  climuzcnv  36058  pocnv  36150  cgrid2  36390  btwncom  36401  btwnswapid2  36405  colinearperm1  36449  colinearperm3  36450  colinearperm2  36451  colinearperm4  36452  lineext  36463  colinbtwnle  36505  broutsideof2  36509  outsideofcom  36515  linecom  36537  linerflx2  36538  lineintmo  36544  fwddifn0  36551  hfext  36570  ntruni  36723  clsint2  36725  neibastop1  36755  weiunlem  36859  bj-snsetex  37483  relowlssretop  37892  pibt2  37946  fin2solem  38140  lindsadd  38147  matunitlindflem1  38150  poimirlem4  38158  poimirlem25  38179  poimirlem32  38186  opnmbllem0  38190  mblfinlem3  38193  mbfposadd  38201  itg2addnclem3  38207  ftc1anclem6  38232  ftc1anc  38235  ac6gf  38266  heibor1lem  38343  isdrngo2  38492  unichnidl  38565  isfldidl  38602  cnf1dd  38624  membpartlem19  39448  lkrss2N  39828  elpadd0  40468  ltrnu  40780  tendoex  41634  cdlemm10N  41777  dicfnN  41842  dihmeetlem2N  41958  dihlatat  41996  lcfrlem9  42209  uzindd  42630  sticksstones1  42798  ofun  42889  nn0addcom  43119  nn0mulcom  43123  zmulcomlem  43124  fsuppind  43207  prjspner1  43243  infdesc  43260  ismrcd1  43314  isnacs3  43326  pellfundglb  43497  jm2.22  43607  jm2.23  43608  isnumbasgrplem1  43713  hbtlem6  43741  rngunsnply  43781  ordsssucim  44014  mnringmulrcld  44837  dvgrat  44907  cvgdvgrat  44908  nznngen  44911  uzmptshftfval  44941  wfac8prim  45596  rnmptlb  45843  rnmptbddlem  45844  rnmptbd2lem  45848  iccshift  46119  iooshift  46123  liminflbuz2  46414  xlimbr  46426  itgperiod  46580  fourierdlem42  46748  fourierdlem68  46773  fourierdlem93  46798  smfpimne2  47439  elprneb  47648  dfatcolem  47874  modmknepk  47987  ichim  48088  ichnfb  48096  prproropf1olem1  48134  prproropf1olem3  48136  gpgnbgrvtx0  48721  gpgnbgrvtx1  48722  2zlidl  48887  lspsslco  49095  isthincd2  50093  fullthinc  50106