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  2628  2eu1  2644  2eu1v  2645  elnelne1  3040  elnelne2  3041  morex  3690  psssstr  4072  reuss2  4289  reupick  4292  reximdva0  4318  falseral0  4479  rabsneu  4693  invdisjrab  5094  opabss  5171  triun  5229  triin  5231  poirr  5558  wefrc  5632  xpcan  6149  fnfco  6725  eqfnun  7009  fnressn  7130  fvtp3  7171  fvtp3g  7174  f1mpt  7236  offval  7662  ordsucuniel  7799  onzsl  7822  soex  7897  fiunlem  7920  fiun  7921  f1iun  7922  dfoprab3  8033  poxp  8107  fnwelem  8110  poxp2  8122  suppssr  8174  suppssrg  8175  suppsssn  8180  suppofssd  8182  fprlem2  8280  oeordsuc  8558  oelim2  8559  omsmolem  8621  rexdif1enOLD  9123  ssnnfi  9133  ssfi  9137  ensymfib  9148  domnsymfi  9164  fiint  9277  fiintOLD  9278  unifi  9295  indexfi  9311  iinfi  9368  unwdomg  9537  inf3lem5  9585  rankr1bg  9756  rankr1c  9774  carden2a  9919  dfac8clem  9985  dfac5lem4  10079  dfac5lem4OLD  10081  pwsdompw  10156  cfsuc  10210  cflim2  10216  enfin2i  10274  isf34lem4  10330  axdc4lem  10408  zornn0g  10458  uniimadomf  10498  fpwwe2lem7  10590  fpwwe2lem11  10594  fpwwe2lem12  10595  pwfseqlem1  10611  pwfseqlem5  10616  intgru  10767  addclpi  10845  addnidpi  10854  ltsonq  10922  nqpr  10967  reclem3pr  11002  recexsr  11060  supsrlem  11064  nnnn0addcl  12472  un0addcl  12475  un0mulcl  12476  nn0nndivcl  12514  nn0ge0div  12603  uzind3  12628  uzind4  12865  zsupss  12896  rpnnen1lem2  12936  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  ltsubrp  12989  ltaddrp  12990  xrlttr  13100  qbtwnxr  13160  xltnegi  13176  xaddnemnf  13196  xaddnepnf  13197  xaddcom  13200  xnegdi  13208  xsubge0  13221  xrub  13272  fzne1  13565  fzind2  13746  seqof  14024  expp1  14033  expneg  14034  expcllem  14037  mulexpz  14067  expaddz  14071  expmulz  14073  faclbnd4lem3  14260  faclbnd4  14262  fi1uzind  14472  swrd00  14609  swrd0  14623  cats1un  14686  reuccatpfxs1  14712  cshw0  14759  cshwn  14762  wwlktovfo  14924  shftf  15045  sqrtdiv  15231  leabs  15265  mulcn2  15562  summolem2  15682  fsumrev2  15748  geomulcvg  15842  prodmolem2  15901  zprod  15903  prodsn  15928  prodsnf  15930  fprodle  15962  bpolydiflem  16020  bpoly2  16023  bpoly3  16024  ruclem6  16203  dvdsflip  16287  dvdsfac  16296  gcdcllem1  16469  lcmgcdlem  16576  rpexp1i  16693  hashdvds  16745  hashgcdlem  16758  phisum  16761  iserodd  16806  pcqcl  16827  pcid  16844  ismred  17563  funcpropd  17864  natpropd  17941  odupos  18287  lubun  18474  rabsubmgmd  18631  sgrpidmnd  18666  issubmd  18733  grpinvnzcl  18943  mulgneg  19024  mulgnn0z  19033  symgfixf1  19367  symgsssg  19397  symgfisg  19398  pgpssslw  19544  sylow2alem2  19548  sylow2a  19549  oddvdssubg  19785  gsumzunsnd  19886  gsumunsnfd  19887  gsum2dlem1  19900  gsum2dlem2  19901  gsumcom3  19908  ablfac1eu  20005  pgpfac1lem5  20011  gsumdixp  20228  dvdsrcl2  20275  01eq0ring  20439  isdrngd  20674  isdrngdOLD  20676  cnsubrg  21344  psgnodpm  21497  evlslem4  21983  psdmul  22053  coe1tmmul2  22162  mpomatmul  22333  cpmidpmat  22760  intcld  22927  neiptopnei  23019  ordtrest2lem  23090  lmss  23185  cmpcovf  23278  cncmp  23279  fincmp  23280  cmpsublem  23286  cmpsub  23287  unconn  23316  1stcfb  23332  2ndcsep  23346  refun0  23402  locfincmp  23413  1stckgenlem  23440  ptbasin  23464  ptbasfi  23468  ptunimpt  23482  ptuniconst  23485  dfac14  23505  ptcnp  23509  xkoptsub  23541  xkococnlem  23546  xkoinjcn  23574  qtopcmplem  23594  qtophmeo  23704  fbfinnfr  23728  isufil2  23795  isfcls  23896  xmetrtri  24243  xmetrtri2  24244  blssioo  24683  divcnOLD  24757  divcn  24759  bndth  24857  clmvscom  24990  resscdrg  25258  minveclem3  25329  finiunmbl  25445  opnmbllem  25502  ismbf2d  25541  itg2seq  25643  bddiblnc  25743  ellimc2  25778  limcmpt2  25785  limcres  25787  dvlem  25797  dvidlem  25816  dvrec  25859  dveflem  25883  dvlip  25898  coe1mul3  26004  dvtaylp  26278  leibpilem2  26851  leibpi  26852  wilthlem2  26979  basellem3  26993  dchreq  27169  dchrsum  27180  lgsval3  27226  lgsdir2lem4  27239  2sqlem6  27334  rpvmasumlem  27398  dchrisum0fno1  27422  rpvmasum2  27423  pntrsumbnd2  27478  ostthlem1  27538  nosupno  27615  negsbdaylem  27962  expsp1  28315  colmid  28615  lmiisolem  28723  dfcgra2  28757  axcontlem2  28892  axcontlem7  28897  upgrex  29019  umgredg  29065  umgrpredgv  29067  umgredgne  29072  umgredgnlp  29074  usgredgppr  29123  edgssv2  29125  uspgredg2vlem  29150  usgredg2vlem1  29152  upgrres1  29240  nbuhgr2vtx1edgblem  29278  nbusgrf1o0  29296  hashnbusgrnn0  29303  iscplgredg  29344  uhgrvd00  29462  finsumvtxdg2size  29478  wlkepvtx  29588  wlknewwlksn  29817  wwlksnextfun  29828  wwlksnextsurj  29830  elwwlks2ons3im  29884  wwlks2onsym  29888  clwwlkf  29976  fusgreghash2wspv  30264  numclwwlk5lem  30316  grpoidinvlem3  30435  ablo32  30478  ablomuldiv  30481  ablodivdiv  30482  ablodiv32  30484  nvscom  30558  dipassr  30775  htthlem  30846  hsn0elch  31177  shscli  31246  nmopun  31943  branmfn  32034  mdslj1i  32248  mdslj2i  32249  atss  32275  chcv1  32284  dmdbr5ati  32351  snsssng  32443  ifnebib  32478  fnpreimac  32595  fcnvgreu  32597  isoun  32625  fsuppcurry1  32648  fsuppcurry2  32649  prodpr  32751  prodtp  32752  pmtrprfv2  33045  elrgspnsubrunlem2  33199  nsgmgclem  33382  nsgqusf1olem2  33385  isprmidlc  33418  ssdifidllem  33427  ssdifidlprm  33429  ssmxidllem  33444  qsdrng  33468  1arithufdlem3  33517  ordtrest2NEWlem  33912  esumsplit  34043  esumpad2  34046  esumpcvgval  34068  sigaclcu2  34110  ldgenpisyslem1  34153  volmeas  34221  mbfmco2  34256  omsmeas  34314  oddpwdc  34345  eulerpartlemgvv  34367  ballotlemfc0  34484  ballotlemfcc  34485  prodfzo03  34594  circlemethhgt  34634  bnj1109  34776  bnj1294  34807  bnj545  34885  bnj605  34897  bnj594  34902  bnj934  34925  bnj953  34929  bnj1137  34985  bnj1174  34993  bnj1388  35023  subfacp1lem4  35170  erdszelem7  35184  erdszelem8  35185  erdsze2lem2  35191  resconn  35233  cvmsdisj  35257  cvmscld  35260  satf0op  35364  mclsax  35556  climuzcnv  35658  pocnv  35750  cgrid2  35991  btwncom  36002  btwnswapid2  36006  colinearperm1  36050  colinearperm3  36051  colinearperm2  36052  colinearperm4  36053  lineext  36064  colinbtwnle  36106  broutsideof2  36110  outsideofcom  36116  linecom  36138  linerflx2  36139  lineintmo  36145  fwddifn0  36152  hfext  36171  ntruni  36315  clsint2  36317  neibastop1  36347  weiunlem2  36451  bj-snsetex  36951  relowlssretop  37351  pibt2  37405  fin2solem  37600  lindsadd  37607  matunitlindflem1  37610  poimirlem4  37618  poimirlem25  37639  poimirlem32  37646  opnmbllem0  37650  mblfinlem3  37653  mbfposadd  37661  itg2addnclem3  37667  ftc1anclem6  37692  ftc1anc  37695  ac6gf  37726  heibor1lem  37803  isdrngo2  37952  unichnidl  38025  isfldidl  38062  cnf1dd  38084  membpartlem19  38803  lkrss2N  39162  elpadd0  39803  ltrnu  40115  tendoex  40969  cdlemm10N  41112  dicfnN  41177  dihmeetlem2N  41293  dihlatat  41331  lcfrlem9  41544  uzindd  41965  sticksstones1  42134  ofun  42224  nn0addcom  42450  nn0mulcom  42454  zmulcomlem  42455  fsuppind  42578  prjspner1  42614  infdesc  42631  ismrcd1  42686  isnacs3  42698  pellfundglb  42873  jm2.22  42984  jm2.23  42985  isnumbasgrplem1  43090  hbtlem6  43118  rngunsnply  43158  ordsssucim  43391  mnringmulrcld  44217  dvgrat  44301  cvgdvgrat  44302  nznngen  44305  uzmptshftfval  44335  wfac8prim  44992  rnmptlb  45237  rnmptbddlem  45238  rnmptbd2lem  45242  iccshift  45516  iooshift  45520  liminflbuz2  45813  xlimbr  45825  itgperiod  45979  fourierdlem42  46147  fourierdlem68  46172  fourierdlem93  46197  smfpimne2  46838  elprneb  47030  dfatcolem  47256  modmknepk  47363  ichim  47458  ichnfb  47466  prproropf1olem1  47504  prproropf1olem3  47506  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  2zlidl  48228  lspsslco  48426  isthincd2  49426  fullthinc  49439