Theorem sylan2b 596

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 595	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

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

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 400

This theorem is referenced by:  syl2anb  600  eupickb  2697  2eu1  2712  2eu1v  2713  eqtr3  2820  elnelne1  3101  elnelne2  3102  morex  3658  psssstr  4034  reuss2  4235  reupick  4239  reximdva0  4265  falseral0  4417  rabsneu  4625  invdisjrabw  5015  opabss  5094  triun  5149  triin  5151  poirr  5449  wefrc  5513  xpcan  6000  fnfco  6517  fnressn  6897  fvtp3  6936  fvtp3g  6939  f1mpt  6997  offval  7396  ordsucuniel  7519  onzsl  7541  soex  7608  fiunlem  7625  fiun  7626  f1iun  7627  dfoprab3  7734  poxp  7805  fnwelem  7808  suppssr  7844  suppsssn  7848  suppofssd  7850  oeordsuc  8203  oelim2  8204  omsmolem  8263  ssnnfi  8721  fiint  8779  unifi  8797  indexfi  8816  iinfi  8865  unwdomg  9032  inf3lem5  9079  rankr1bg  9216  rankr1c  9234  carden2a  9379  dfac8clem  9443  dfac5lem4  9537  pwsdompw  9615  cfsuc  9668  cflim2  9674  enfin2i  9732  isf34lem4  9788  axdc4lem  9866  zornn0g  9916  uniimadomf  9956  fpwwe2lem8  10048  fpwwe2lem12  10052  fpwwe2lem13  10053  pwfseqlem1  10069  pwfseqlem5  10074  intgru  10225  addclpi  10303  addnidpi  10312  ltsonq  10380  nqpr  10425  reclem3pr  10460  recexsr  10518  supsrlem  10522  nnnn0addcl  11915  un0addcl  11918  un0mulcl  11919  nn0nndivcl  11954  nn0ge0div  12039  uzind3  12064  uzind4  12294  zsupss  12325  rpnnen1lem2  12364  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  ltsubrp  12413  ltaddrp  12414  xrlttr  12521  qbtwnxr  12581  xltnegi  12597  xaddnemnf  12617  xaddnepnf  12618  xaddcom  12621  xnegdi  12629  xsubge0  12642  xrub  12693  fzind2  13150  seqof  13423  expp1  13432  expneg  13433  expcllem  13436  mulexpz  13465  expaddz  13469  expmulz  13471  faclbnd4lem3  13651  faclbnd4  13653  fi1uzind  13851  swrd00  13997  swrd0  14011  cats1un  14074  reuccatpfxs1  14100  cshw0  14147  cshwn  14150  wwlktovfo  14313  shftf  14430  sqrtdiv  14617  leabs  14651  mulcn2  14944  summolem2  15065  fsumrev2  15129  geomulcvg  15224  prodmolem2  15281  zprod  15283  prodsn  15308  prodsnf  15310  fprodle  15342  bpolydiflem  15400  bpoly2  15403  bpoly3  15404  ruclem6  15580  dvdsflip  15659  dvdsfac  15668  gcdcllem1  15838  lcmgcdlem  15940  rpexp1i  16055  hashdvds  16102  hashgcdlem  16115  phisum  16117  iserodd  16162  pcqcl  16183  pcid  16199  ismred  16865  funcpropd  17162  natpropd  17238  lubun  17725  odupos  17737  sgrpidmnd  17908  issubmd  17963  grpinvnzcl  18163  mulgneg  18238  mulgnn0z  18246  symgfixf1  18557  symgsssg  18587  symgfisg  18588  pgpssslw  18731  sylow2alem2  18735  sylow2a  18736  oddvdssubg  18968  gsumzunsnd  19069  gsumunsnfd  19070  gsum2dlem1  19083  gsum2dlem2  19084  gsumcom3  19091  ablfac1eu  19188  pgpfac1lem5  19194  gsumdixp  19355  dvdsrcl2  19396  isdrngd  19520  cnsubrg  20151  psgnodpm  20277  evlslem4  20747  coe1tmmul2  20905  mpomatmul  21051  cpmidpmat  21478  intcld  21645  neiptopnei  21737  ordtrest2lem  21808  lmss  21903  cmpcovf  21996  cncmp  21997  fincmp  21998  cmpsublem  22004  cmpsub  22005  unconn  22034  1stcfb  22050  2ndcsep  22064  refun0  22120  locfincmp  22131  1stckgenlem  22158  ptbasin  22182  ptbasfi  22186  ptunimpt  22200  ptuniconst  22203  dfac14  22223  ptcnp  22227  xkoptsub  22259  xkococnlem  22264  xkoinjcn  22292  qtopcmplem  22312  qtophmeo  22422  fbfinnfr  22446  isufil2  22513  isfcls  22614  xmetrtri  22962  xmetrtri2  22963  blssioo  23400  divcn  23473  bndth  23563  clmvscom  23695  resscdrg  23962  minveclem3  24033  finiunmbl  24148  opnmbllem  24205  ismbf2d  24244  itg2seq  24346  bddiblnc  24445  ellimc2  24480  limcmpt2  24487  limcres  24489  dvlem  24499  dvidlem  24518  dvrec  24558  dveflem  24582  dvlip  24596  coe1mul3  24700  dvtaylp  24965  leibpilem2  25527  leibpi  25528  wilthlem2  25654  basellem3  25668  dchreq  25842  dchrsum  25853  lgsval3  25899  lgsdir2lem4  25912  2sqlem6  26007  rpvmasumlem  26071  dchrisum0fno1  26095  rpvmasum2  26096  pntrsumbnd2  26151  ostthlem1  26211  colmid  26482  lmiisolem  26590  dfcgra2  26624  axcontlem2  26759  axcontlem7  26764  upgrex  26885  umgredg  26931  umgrpredgv  26933  umgredgne  26938  umgredgnlp  26940  usgredgppr  26986  edgssv2  26988  uspgredg2vlem  27013  usgredg2vlem1  27015  upgrres1  27103  nbuhgr2vtx1edgblem  27141  nbusgrf1o0  27159  hashnbusgrnn0  27166  iscplgredg  27207  uhgrvd00  27324  finsumvtxdg2size  27340  wlkepvtx  27450  wlknewwlksn  27673  wwlksnextfun  27684  wwlksnextsurj  27686  elwwlks2ons3im  27740  wwlks2onsym  27744  clwwlkf  27832  fusgreghash2wspv  28120  numclwwlk5lem  28172  grpoidinvlem3  28289  ablo32  28332  ablomuldiv  28335  ablodivdiv  28336  ablodiv32  28338  nvscom  28412  dipassr  28629  htthlem  28700  hsn0elch  29031  shscli  29100  nmopun  29797  branmfn  29888  mdslj1i  30102  mdslj2i  30103  atss  30129  chcv1  30138  dmdbr5ati  30205  snsssng  30284  fnpreimac  30434  fcnvgreu  30436  isoun  30461  fsuppcurry1  30487  fsuppcurry2  30488  fzne1  30537  prodpr  30568  prodtp  30569  pmtrprfv2  30782  isprmidlc  31031  ssmxidllem  31049  ordtrest2NEWlem  31275  esumsplit  31422  esumpad2  31425  esumpcvgval  31447  sigaclcu2  31489  ldgenpisyslem1  31532  volmeas  31600  mbfmco2  31633  omsmeas  31691  oddpwdc  31722  eulerpartlemgvv  31744  ballotlemfc0  31860  ballotlemfcc  31861  prodfzo03  31984  circlemethhgt  32024  bnj521  32117  bnj1109  32168  bnj1294  32199  bnj545  32277  bnj605  32289  bnj594  32294  bnj934  32317  bnj953  32321  bnj1137  32377  bnj1174  32385  bnj1388  32415  subfacp1lem4  32543  erdszelem7  32557  erdszelem8  32558  erdsze2lem2  32564  resconn  32606  cvmsdisj  32630  cvmscld  32633  satf0op  32737  mclsax  32929  climuzcnv  33027  pocnv  33112  trpredmintr  33183  fprlem2  33251  nosupno  33316  cgrid2  33577  btwncom  33588  btwnswapid2  33592  colinearperm1  33636  colinearperm3  33637  colinearperm2  33638  colinearperm4  33639  lineext  33650  colinbtwnle  33692  broutsideof2  33696  outsideofcom  33702  linecom  33724  linerflx2  33725  lineintmo  33731  fwddifn0  33738  hfext  33757  ntruni  33788  clsint2  33790  neibastop1  33820  bj-snsetex  34399  relowlssretop  34780  pibt2  34834  fin2solem  35043  lindsadd  35050  matunitlindflem1  35053  poimirlem4  35061  poimirlem25  35082  poimirlem32  35089  opnmbllem0  35093  mblfinlem3  35096  mbfposadd  35104  itg2addnclem3  35110  ftc1anclem6  35135  ftc1anc  35138  eqfnun  35160  ac6gf  35170  heibor1lem  35247  isdrngo2  35396  unichnidl  35469  isfldidl  35506  cnf1dd  35528  lkrss2N  36465  elpadd0  37105  ltrnu  37417  tendoex  38271  cdlemm10N  38414  dicfnN  38479  dihmeetlem2N  38595  dihlatat  38633  lcfrlem9  38846  uzindd  39264  metakunt12  39361  ofun  39416  fsuppind  39456  ismrcd1  39639  isnacs3  39651  pellfundglb  39826  jm2.22  39936  jm2.23  39937  isnumbasgrplem1  40045  hbtlem6  40073  rngunsnply  40117  mnringmulrcld  40936  dvgrat  41016  cvgdvgrat  41017  nznngen  41020  uzmptshftfval  41050  rnmptlb  41880  rnmptbddlem  41881  rnmptbd2lem  41886  iccshift  42155  iooshift  42159  liminflbuz2  42457  xlimbr  42469  itgperiod  42623  fourierdlem42  42791  fourierdlem68  42816  fourierdlem93  42841  elprneb  43621  dfatcolem  43811  ichim  43974  ichnfb  43982  prproropf1olem1  44020  prproropf1olem3  44022  rabsubmgmd  44411  2zlidl  44558  lspsslco  44846