Theorem sylan2b 600

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  syl2anb  604  eupickb  2639  2eu1  2655  2eu1v  2656  elnelne1  3050  elnelne2  3051  morex  3667  psssstr  4047  reuss2  4261  reupick  4264  reximdva0  4290  falseral0OLD  4450  rabsneu  4668  invdisjrab  5066  opabss  5143  triun  5201  triin  5203  poirr  5545  wefrc  5619  xpcan  6134  fnfco  6699  eqfnun  6985  fnressn  7108  fvtp3  7148  fvtp3g  7151  f1mpt  7212  offval  7636  ordsucuniel  7771  onzsl  7793  soex  7868  fiunlem  7891  fiun  7892  f1iun  7893  dfoprab3  8003  poxp  8075  fnwelem  8078  poxp2  8090  suppssr  8142  suppssrg  8143  suppsssn  8148  suppofssd  8150  fprlem2  8248  oeordsuc  8527  oelim2  8528  omsmolem  8590  ssnnfi  9101  ssfi  9104  ensymfib  9115  domnsymfi  9131  fiint  9234  unifi  9251  indexfi  9267  iinfi  9327  unwdomg  9496  inf3lem5  9551  rankr1bg  9725  rankr1c  9743  carden2a  9888  dfac8clem  9952  dfac5lem4  10046  dfac5lem4OLD  10048  pwsdompw  10123  cfsuc  10177  cflim2  10183  enfin2i  10241  isf34lem4  10297  axdc4lem  10375  zornn0g  10425  uniimadomf  10465  fpwwe2lem7  10558  fpwwe2lem11  10562  fpwwe2lem12  10563  pwfseqlem1  10579  pwfseqlem5  10584  intgru  10735  addclpi  10813  addnidpi  10822  ltsonq  10890  nqpr  10935  reclem3pr  10970  recexsr  11028  supsrlem  11032  nnnn0addcl  12465  un0addcl  12468  un0mulcl  12469  nn0nndivcl  12507  nn0ge0div  12596  uzind3  12621  uzind4  12854  zsupss  12885  rpnnen1lem2  12925  rpnnen1lem1  12926  rpnnen1lem3  12927  rpnnen1lem5  12929  ltsubrp  12978  ltaddrp  12979  xrlttr  13089  qbtwnxr  13150  xltnegi  13166  xaddnemnf  13186  xaddnepnf  13187  xaddcom  13190  xnegdi  13198  xsubge0  13211  xrub  13262  fzne1  13556  fzind2  13741  seqof  14019  expp1  14028  expneg  14029  expcllem  14032  mulexpz  14062  expaddz  14066  expmulz  14068  faclbnd4lem3  14255  faclbnd4  14257  fi1uzind  14467  swrd00  14605  swrd0  14619  cats1un  14681  reuccatpfxs1  14707  cshw0  14754  cshwn  14757  wwlktovfo  14918  shftf  15039  sqrtdiv  15225  leabs  15259  mulcn2  15556  summolem2  15676  fsumrev2  15742  geomulcvg  15839  prodmolem2  15898  zprod  15900  prodsn  15925  prodsnf  15927  fprodle  15959  bpolydiflem  16017  bpoly2  16020  bpoly3  16021  ruclem6  16200  dvdsflip  16284  dvdsfac  16293  gcdcllem1  16466  lcmgcdlem  16573  rpexp1i  16691  hashdvds  16743  hashgcdlem  16756  phisum  16759  iserodd  16804  pcqcl  16825  pcid  16842  ismred  17562  funcpropd  17867  natpropd  17944  odupos  18290  lubun  18479  rabsubmgmd  18670  sgrpidmnd  18705  issubmd  18772  grpinvnzcl  18985  mulgneg  19066  mulgnn0z  19075  symgfixf1  19410  symgsssg  19440  symgfisg  19441  pgpssslw  19587  sylow2alem2  19591  sylow2a  19592  oddvdssubg  19828  gsumzunsnd  19929  gsumunsnfd  19930  gsum2dlem1  19943  gsum2dlem2  19944  gsumcom3  19951  ablfac1eu  20048  pgpfac1lem5  20054  gsumdixp  20296  dvdsrcl2  20344  01eq0ring  20509  isdrngd  20744  isdrngdOLD  20746  cnsubrg  21409  psgnodpm  21570  evlslem4  22059  psdmul  22161  coe1tmmul2  22269  mpomatmul  22436  cpmidpmat  22863  intcld  23030  neiptopnei  23122  ordtrest2lem  23193  lmss  23288  cmpcovf  23381  cncmp  23382  fincmp  23383  cmpsublem  23389  cmpsub  23390  unconn  23419  1stcfb  23435  2ndcsep  23449  refun0  23505  locfincmp  23516  1stckgenlem  23543  ptbasin  23567  ptbasfi  23571  ptunimpt  23585  ptuniconst  23588  dfac14  23608  ptcnp  23612  xkoptsub  23644  xkococnlem  23649  xkoinjcn  23677  qtopcmplem  23697  qtophmeo  23807  fbfinnfr  23831  isufil2  23898  isfcls  23999  xmetrtri  24345  xmetrtri2  24346  blssioo  24785  divcn  24860  bndth  24950  clmvscom  25082  resscdrg  25350  minveclem3  25421  finiunmbl  25536  opnmbllem  25593  ismbf2d  25632  itg2seq  25734  bddiblnc  25834  ellimc2  25869  limcmpt2  25876  limcres  25878  dvlem  25888  dvidlem  25907  dvrec  25947  dveflem  25971  dvlip  25985  coe1mul3  26089  dvtaylp  26360  leibpilem2  26930  leibpi  26931  wilthlem2  27057  basellem3  27071  dchreq  27246  dchrsum  27257  lgsval3  27303  lgsdir2lem4  27316  2sqlem6  27411  rpvmasumlem  27475  dchrisum0fno1  27499  rpvmasum2  27500  pntrsumbnd2  27555  ostthlem1  27615  nosupno  27692  negbdaylem  28073  expsp1  28446  colmid  28781  lmiisolem  28889  dfcgra2  28923  axcontlem2  29059  axcontlem7  29064  upgrex  29186  umgredg  29232  umgrpredgv  29234  umgredgne  29239  umgredgnlp  29241  usgredgppr  29290  edgssv2  29292  uspgredg2vlem  29317  usgredg2vlem1  29319  upgrres1  29407  nbuhgr2vtx1edgblem  29445  nbusgrf1o0  29463  hashnbusgrnn0  29470  iscplgredg  29511  uhgrvd00  29628  finsumvtxdg2size  29644  wlkepvtx  29752  wlknewwlksn  29980  wwlksnextfun  29991  wwlksnextsurj  29993  elwwlks2ons3im  30047  wwlks2onsym  30053  clwwlkf  30142  fusgreghash2wspv  30430  numclwwlk5lem  30482  grpoidinvlem3  30602  ablo32  30645  ablomuldiv  30648  ablodivdiv  30649  ablodiv32  30651  nvscom  30725  dipassr  30942  htthlem  31013  hsn0elch  31344  shscli  31413  nmopun  32110  branmfn  32201  mdslj1i  32415  mdslj2i  32416  atss  32442  chcv1  32451  dmdbr5ati  32518  snsssng  32609  ifnebib  32644  fnpreimac  32769  fcnvgreu  32771  isoun  32801  fsuppcurry1  32823  fsuppcurry2  32824  prodpr  32925  prodtp  32926  pmtrprfv2  33176  elrgspnsubrunlem2  33336  nsgmgclem  33501  nsgqusf1olem2  33504  isprmidlc  33537  ssdifidllem  33546  ssdifidlprm  33548  ssmxidllem  33563  qsdrng  33587  1arithufdlem3  33636  ordtrest2NEWlem  34113  esumsplit  34244  esumpad2  34247  esumpcvgval  34269  sigaclcu2  34311  ldgenpisyslem1  34354  volmeas  34422  mbfmco2  34456  omsmeas  34514  oddpwdc  34545  eulerpartlemgvv  34567  ballotlemfc0  34684  ballotlemfcc  34685  prodfzo03  34794  circlemethhgt  34834  bnj1109  34976  bnj1294  35006  bnj545  35084  bnj605  35096  bnj594  35101  bnj934  35124  bnj953  35128  bnj1137  35184  bnj1174  35192  bnj1388  35222  subfacp1lem4  35418  erdszelem7  35432  erdszelem8  35433  erdsze2lem2  35439  resconn  35481  cvmsdisj  35505  cvmscld  35508  satf0op  35612  mclsax  35804  climuzcnv  35906  pocnv  35998  cgrid2  36238  btwncom  36249  btwnswapid2  36253  colinearperm1  36297  colinearperm3  36298  colinearperm2  36299  colinearperm4  36300  lineext  36311  colinbtwnle  36353  broutsideof2  36357  outsideofcom  36363  linecom  36385  linerflx2  36386  lineintmo  36392  fwddifn0  36399  hfext  36418  ntruni  36562  clsint2  36564  neibastop1  36594  weiunlem  36698  bj-snsetex  37323  relowlssretop  37732  pibt2  37786  fin2solem  37980  lindsadd  37987  matunitlindflem1  37990  poimirlem4  37998  poimirlem25  38019  poimirlem32  38026  opnmbllem0  38030  mblfinlem3  38033  mbfposadd  38041  itg2addnclem3  38047  ftc1anclem6  38072  ftc1anc  38075  ac6gf  38106  heibor1lem  38183  isdrngo2  38332  unichnidl  38405  isfldidl  38442  cnf1dd  38464  membpartlem19  39288  lkrss2N  39668  elpadd0  40308  ltrnu  40620  tendoex  41474  cdlemm10N  41617  dicfnN  41682  dihmeetlem2N  41798  dihlatat  41836  lcfrlem9  42049  uzindd  42470  sticksstones1  42638  ofun  42729  nn0addcom  42959  nn0mulcom  42963  zmulcomlem  42964  fsuppind  43047  prjspner1  43083  infdesc  43100  ismrcd1  43154  isnacs3  43166  pellfundglb  43337  jm2.22  43447  jm2.23  43448  isnumbasgrplem1  43553  hbtlem6  43581  rngunsnply  43621  ordsssucim  43854  mnringmulrcld  44679  dvgrat  44763  cvgdvgrat  44764  nznngen  44767  uzmptshftfval  44797  wfac8prim  45453  rnmptlb  45694  rnmptbddlem  45695  rnmptbd2lem  45699  iccshift  45970  iooshift  45974  liminflbuz2  46265  xlimbr  46277  itgperiod  46431  fourierdlem42  46599  fourierdlem68  46624  fourierdlem93  46649  smfpimne2  47290  elprneb  47499  dfatcolem  47725  modmknepk  47838  ichim  47939  ichnfb  47947  prproropf1olem1  47985  prproropf1olem3  47987  gpgnbgrvtx0  48572  gpgnbgrvtx1  48573  2zlidl  48738  lspsslco  48935  isthincd2  49934  fullthinc  49947