Theorem sylan2b 592

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  syl2anb  596  eupickb  2627  2eu1  2643  2eu1v  2644  eqtr3OLD  2756  elnelne1  3050  elnelne2  3051  morex  3725  psssstr  4115  reuss2  4328  reupick  4331  reximdva0  4361  falseral0  4527  rabsneu  4741  invdisjrab  5143  opabss  5220  triun  5288  triin  5290  poirr  5610  wefrc  5680  xpcan  6192  fnfco  6771  eqfnun  7055  fnressn  7177  fvtp3  7219  fvtp3g  7222  f1mpt  7281  offval  7704  ordsucuniel  7841  onzsl  7864  soex  7942  fiunlem  7963  fiun  7964  f1iun  7965  dfoprab3  8076  poxp  8150  fnwelem  8153  poxp2  8165  suppssr  8218  suppssrg  8219  suppsssn  8224  suppofssd  8226  fprlem2  8324  oeordsuc  8632  oelim2  8633  omsmolem  8695  rexdif1enOLD  9204  ssnnfi  9214  ssnnfiOLD  9215  ssfi  9219  ensymfib  9229  domnsymfi  9245  fiint  9375  fiintOLD  9376  unifi  9393  indexfi  9411  iinfi  9467  unwdomg  9634  inf3lem5  9682  rankr1bg  9853  rankr1c  9871  carden2a  10016  dfac8clem  10082  dfac5lem4  10176  dfac5lem4OLD  10178  pwsdompw  10253  cfsuc  10307  cflim2  10313  enfin2i  10371  isf34lem4  10427  axdc4lem  10505  zornn0g  10555  uniimadomf  10595  fpwwe2lem7  10687  fpwwe2lem11  10691  fpwwe2lem12  10692  pwfseqlem1  10708  pwfseqlem5  10713  intgru  10864  addclpi  10942  addnidpi  10951  ltsonq  11019  nqpr  11064  reclem3pr  11099  recexsr  11157  supsrlem  11161  nnnn0addcl  12564  un0addcl  12567  un0mulcl  12568  nn0nndivcl  12605  nn0ge0div  12693  uzind3  12718  uzind4  12952  zsupss  12983  rpnnen1lem2  13023  rpnnen1lem1  13024  rpnnen1lem3  13025  rpnnen1lem5  13027  ltsubrp  13074  ltaddrp  13075  xrlttr  13183  qbtwnxr  13243  xltnegi  13259  xaddnemnf  13279  xaddnepnf  13280  xaddcom  13283  xnegdi  13291  xsubge0  13304  xrub  13355  fzind2  13815  seqof  14090  expp1  14099  expneg  14100  expcllem  14103  mulexpz  14133  expaddz  14137  expmulz  14139  faclbnd4lem3  14324  faclbnd4  14326  fi1uzind  14537  swrd00  14673  swrd0  14687  cats1un  14750  reuccatpfxs1  14776  cshw0  14823  cshwn  14826  wwlktovfo  14988  shftf  15105  sqrtdiv  15291  leabs  15325  mulcn2  15619  summolem2  15741  fsumrev2  15807  geomulcvg  15901  prodmolem2  15958  zprod  15960  prodsn  15985  prodsnf  15987  fprodle  16019  bpolydiflem  16077  bpoly2  16080  bpoly3  16081  ruclem6  16258  dvdsflip  16340  dvdsfac  16349  gcdcllem1  16520  lcmgcdlem  16628  rpexp1i  16746  hashdvds  16798  hashgcdlem  16811  phisum  16813  iserodd  16858  pcqcl  16879  pcid  16896  ismred  17636  funcpropd  17943  natpropd  18022  odupos  18374  lubun  18561  rabsubmgmd  18718  sgrpidmnd  18753  issubmd  18817  grpinvnzcl  19027  mulgneg  19108  mulgnn0z  19117  symgfixf1  19457  symgsssg  19487  symgfisg  19488  pgpssslw  19634  sylow2alem2  19638  sylow2a  19639  oddvdssubg  19875  gsumzunsnd  19976  gsumunsnfd  19977  gsum2dlem1  19990  gsum2dlem2  19991  gsumcom3  19998  ablfac1eu  20095  pgpfac1lem5  20101  gsumdixp  20320  dvdsrcl2  20370  01eq0ring  20534  isdrngd  20765  isdrngdOLD  20767  cnsubrg  21446  psgnodpm  21606  evlslem4  22111  psdmul  22182  coe1tmmul2  22289  mpomatmul  22462  cpmidpmat  22889  intcld  23058  neiptopnei  23150  ordtrest2lem  23221  lmss  23316  cmpcovf  23409  cncmp  23410  fincmp  23411  cmpsublem  23417  cmpsub  23418  unconn  23447  1stcfb  23463  2ndcsep  23477  refun0  23533  locfincmp  23544  1stckgenlem  23571  ptbasin  23595  ptbasfi  23599  ptunimpt  23613  ptuniconst  23616  dfac14  23636  ptcnp  23640  xkoptsub  23672  xkococnlem  23677  xkoinjcn  23705  qtopcmplem  23725  qtophmeo  23835  fbfinnfr  23859  isufil2  23926  isfcls  24027  xmetrtri  24375  xmetrtri2  24376  blssioo  24825  divcnOLD  24898  divcn  24900  bndth  24998  clmvscom  25131  resscdrg  25400  minveclem3  25471  finiunmbl  25587  opnmbllem  25644  ismbf2d  25683  itg2seq  25786  bddiblnc  25885  ellimc2  25920  limcmpt2  25927  limcres  25929  dvlem  25939  dvidlem  25958  dvrec  26001  dveflem  26025  dvlip  26040  coe1mul3  26149  dvtaylp  26421  leibpilem2  26992  leibpi  26993  wilthlem2  27120  basellem3  27134  dchreq  27310  dchrsum  27321  lgsval3  27367  lgsdir2lem4  27380  2sqlem6  27475  rpvmasumlem  27539  dchrisum0fno1  27563  rpvmasum2  27564  pntrsumbnd2  27619  ostthlem1  27679  nosupno  27756  negsbdaylem  28088  colmid  28638  lmiisolem  28746  dfcgra2  28780  axcontlem2  28922  axcontlem7  28927  upgrex  29051  umgredg  29097  umgrpredgv  29099  umgredgne  29104  umgredgnlp  29106  usgredgppr  29155  edgssv2  29157  uspgredg2vlem  29182  usgredg2vlem1  29184  upgrres1  29272  nbuhgr2vtx1edgblem  29310  nbusgrf1o0  29328  hashnbusgrnn0  29335  iscplgredg  29376  uhgrvd00  29494  finsumvtxdg2size  29510  wlkepvtx  29620  wlknewwlksn  29844  wwlksnextfun  29855  wwlksnextsurj  29857  elwwlks2ons3im  29911  wwlks2onsym  29915  clwwlkf  30003  fusgreghash2wspv  30291  numclwwlk5lem  30343  grpoidinvlem3  30462  ablo32  30505  ablomuldiv  30508  ablodivdiv  30509  ablodiv32  30511  nvscom  30585  dipassr  30802  htthlem  30873  hsn0elch  31204  shscli  31273  nmopun  31970  branmfn  32061  mdslj1i  32275  mdslj2i  32276  atss  32302  chcv1  32311  dmdbr5ati  32378  snsssng  32467  ifnebib  32496  fnpreimac  32614  fcnvgreu  32616  isoun  32638  fsuppcurry1  32664  fsuppcurry2  32665  fzne1  32718  prodpr  32755  prodtp  32756  pmtrprfv2  32995  nsgmgclem  33317  nsgqusf1olem2  33320  isprmidlc  33353  ssdifidllem  33362  ssdifidlprm  33364  ssmxidllem  33379  qsdrng  33403  1arithufdlem3  33452  ordtrest2NEWlem  33775  esumsplit  33924  esumpad2  33927  esumpcvgval  33949  sigaclcu2  33991  ldgenpisyslem1  34034  volmeas  34102  mbfmco2  34137  omsmeas  34195  oddpwdc  34226  eulerpartlemgvv  34248  ballotlemfc0  34364  ballotlemfcc  34365  prodfzo03  34487  circlemethhgt  34527  bnj1109  34669  bnj1294  34700  bnj545  34778  bnj605  34790  bnj594  34795  bnj934  34818  bnj953  34822  bnj1137  34878  bnj1174  34886  bnj1388  34916  subfacp1lem4  35058  erdszelem7  35072  erdszelem8  35073  erdsze2lem2  35079  resconn  35121  cvmsdisj  35145  cvmscld  35148  satf0op  35252  mclsax  35444  climuzcnv  35546  pocnv  35632  cgrid2  35874  btwncom  35885  btwnswapid2  35889  colinearperm1  35933  colinearperm3  35934  colinearperm2  35935  colinearperm4  35936  lineext  35947  colinbtwnle  35989  broutsideof2  35993  outsideofcom  35999  linecom  36021  linerflx2  36022  lineintmo  36028  fwddifn0  36035  hfext  36054  ntruni  36087  clsint2  36089  neibastop1  36119  bj-snsetex  36717  relowlssretop  37117  pibt2  37171  fin2solem  37354  lindsadd  37361  matunitlindflem1  37364  poimirlem4  37372  poimirlem25  37393  poimirlem32  37400  opnmbllem0  37404  mblfinlem3  37407  mbfposadd  37415  itg2addnclem3  37421  ftc1anclem6  37446  ftc1anc  37449  ac6gf  37480  heibor1lem  37557  isdrngo2  37706  unichnidl  37779  isfldidl  37816  cnf1dd  37838  membpartlem19  38556  lkrss2N  38914  elpadd0  39555  ltrnu  39867  tendoex  40721  cdlemm10N  40864  dicfnN  40929  dihmeetlem2N  41045  dihlatat  41083  lcfrlem9  41296  uzindd  41722  sticksstones1  41892  metakunt12  41958  ofun  42016  nn0addcom  42195  nn0mulcom  42199  zmulcomlem  42200  fsuppind  42314  prjspner1  42350  infdesc  42367  ismrcd1  42426  isnacs3  42438  pellfundglb  42613  jm2.22  42724  jm2.23  42725  isnumbasgrplem1  42833  hbtlem6  42861  rngunsnply  42905  ordsssucim  43140  mnringmulrcld  43973  dvgrat  44057  cvgdvgrat  44058  nznngen  44061  uzmptshftfval  44091  rnmptlb  44922  rnmptbddlem  44923  rnmptbd2lem  44927  iccshift  45206  iooshift  45210  liminflbuz2  45506  xlimbr  45518  itgperiod  45672  fourierdlem42  45840  fourierdlem68  45865  fourierdlem93  45890  smfpimne2  46531  elprneb  46714  dfatcolem  46938  ichim  47099  ichnfb  47107  prproropf1olem1  47145  prproropf1olem3  47147  2zlidl  47698  lspsslco  47901  isthincd2  48440  fullthinc  48448