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  2635  2eu1  2651  2eu1v  2652  elnelne1  3047  elnelne2  3048  morex  3677  psssstr  4061  reuss2  4278  reupick  4281  reximdva0  4307  falseral0OLD  4468  rabsneu  4686  invdisjrab  5085  opabss  5162  triun  5219  triin  5221  poirr  5544  wefrc  5618  xpcan  6134  fnfco  6699  eqfnun  6982  fnressn  7103  fvtp3  7143  fvtp3g  7146  f1mpt  7207  offval  7631  ordsucuniel  7766  onzsl  7788  soex  7863  fiunlem  7886  fiun  7887  f1iun  7888  dfoprab3  7998  poxp  8070  fnwelem  8073  poxp2  8085  suppssr  8137  suppssrg  8138  suppsssn  8143  suppofssd  8145  fprlem2  8243  oeordsuc  8522  oelim2  8523  omsmolem  8585  ssnnfi  9094  ssfi  9097  ensymfib  9108  domnsymfi  9124  fiint  9227  unifi  9244  indexfi  9260  iinfi  9320  unwdomg  9489  inf3lem5  9541  rankr1bg  9715  rankr1c  9733  carden2a  9878  dfac8clem  9942  dfac5lem4  10036  dfac5lem4OLD  10038  pwsdompw  10113  cfsuc  10167  cflim2  10173  enfin2i  10231  isf34lem4  10287  axdc4lem  10365  zornn0g  10415  uniimadomf  10455  fpwwe2lem7  10548  fpwwe2lem11  10552  fpwwe2lem12  10553  pwfseqlem1  10569  pwfseqlem5  10574  intgru  10725  addclpi  10803  addnidpi  10812  ltsonq  10880  nqpr  10925  reclem3pr  10960  recexsr  11018  supsrlem  11022  nnnn0addcl  12431  un0addcl  12434  un0mulcl  12435  nn0nndivcl  12473  nn0ge0div  12561  uzind3  12586  uzind4  12819  zsupss  12850  rpnnen1lem2  12890  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  ltsubrp  12943  ltaddrp  12944  xrlttr  13054  qbtwnxr  13115  xltnegi  13131  xaddnemnf  13151  xaddnepnf  13152  xaddcom  13155  xnegdi  13163  xsubge0  13176  xrub  13227  fzne1  13520  fzind2  13704  seqof  13982  expp1  13991  expneg  13992  expcllem  13995  mulexpz  14025  expaddz  14029  expmulz  14031  faclbnd4lem3  14218  faclbnd4  14220  fi1uzind  14430  swrd00  14568  swrd0  14582  cats1un  14644  reuccatpfxs1  14670  cshw0  14717  cshwn  14720  wwlktovfo  14881  shftf  15002  sqrtdiv  15188  leabs  15222  mulcn2  15519  summolem2  15639  fsumrev2  15705  geomulcvg  15799  prodmolem2  15858  zprod  15860  prodsn  15885  prodsnf  15887  fprodle  15919  bpolydiflem  15977  bpoly2  15980  bpoly3  15981  ruclem6  16160  dvdsflip  16244  dvdsfac  16253  gcdcllem1  16426  lcmgcdlem  16533  rpexp1i  16650  hashdvds  16702  hashgcdlem  16715  phisum  16718  iserodd  16763  pcqcl  16784  pcid  16801  ismred  17521  funcpropd  17826  natpropd  17903  odupos  18249  lubun  18438  rabsubmgmd  18629  sgrpidmnd  18664  issubmd  18731  grpinvnzcl  18941  mulgneg  19022  mulgnn0z  19031  symgfixf1  19366  symgsssg  19396  symgfisg  19397  pgpssslw  19543  sylow2alem2  19547  sylow2a  19548  oddvdssubg  19784  gsumzunsnd  19885  gsumunsnfd  19886  gsum2dlem1  19899  gsum2dlem2  19900  gsumcom3  19907  ablfac1eu  20004  pgpfac1lem5  20010  gsumdixp  20254  dvdsrcl2  20302  01eq0ring  20463  isdrngd  20698  isdrngdOLD  20700  cnsubrg  21382  psgnodpm  21543  evlslem4  22031  psdmul  22109  coe1tmmul2  22218  mpomatmul  22390  cpmidpmat  22817  intcld  22984  neiptopnei  23076  ordtrest2lem  23147  lmss  23242  cmpcovf  23335  cncmp  23336  fincmp  23337  cmpsublem  23343  cmpsub  23344  unconn  23373  1stcfb  23389  2ndcsep  23403  refun0  23459  locfincmp  23470  1stckgenlem  23497  ptbasin  23521  ptbasfi  23525  ptunimpt  23539  ptuniconst  23542  dfac14  23562  ptcnp  23566  xkoptsub  23598  xkococnlem  23603  xkoinjcn  23631  qtopcmplem  23651  qtophmeo  23761  fbfinnfr  23785  isufil2  23852  isfcls  23953  xmetrtri  24299  xmetrtri2  24300  blssioo  24739  divcnOLD  24813  divcn  24815  bndth  24913  clmvscom  25046  resscdrg  25314  minveclem3  25385  finiunmbl  25501  opnmbllem  25558  ismbf2d  25597  itg2seq  25699  bddiblnc  25799  ellimc2  25834  limcmpt2  25841  limcres  25843  dvlem  25853  dvidlem  25872  dvrec  25915  dveflem  25939  dvlip  25954  coe1mul3  26060  dvtaylp  26334  leibpilem2  26907  leibpi  26908  wilthlem2  27035  basellem3  27049  dchreq  27225  dchrsum  27236  lgsval3  27282  lgsdir2lem4  27295  2sqlem6  27390  rpvmasumlem  27454  dchrisum0fno1  27478  rpvmasum2  27479  pntrsumbnd2  27534  ostthlem1  27594  nosupno  27671  negbdaylem  28052  expsp1  28425  colmid  28760  lmiisolem  28868  dfcgra2  28902  axcontlem2  29038  axcontlem7  29043  upgrex  29165  umgredg  29211  umgrpredgv  29213  umgredgne  29218  umgredgnlp  29220  usgredgppr  29269  edgssv2  29271  uspgredg2vlem  29296  usgredg2vlem1  29298  upgrres1  29386  nbuhgr2vtx1edgblem  29424  nbusgrf1o0  29442  hashnbusgrnn0  29449  iscplgredg  29490  uhgrvd00  29608  finsumvtxdg2size  29624  wlkepvtx  29732  wlknewwlksn  29960  wwlksnextfun  29971  wwlksnextsurj  29973  elwwlks2ons3im  30027  wwlks2onsym  30033  clwwlkf  30122  fusgreghash2wspv  30410  numclwwlk5lem  30462  grpoidinvlem3  30581  ablo32  30624  ablomuldiv  30627  ablodivdiv  30628  ablodiv32  30630  nvscom  30704  dipassr  30921  htthlem  30992  hsn0elch  31323  shscli  31392  nmopun  32089  branmfn  32180  mdslj1i  32394  mdslj2i  32395  atss  32421  chcv1  32430  dmdbr5ati  32497  snsssng  32589  ifnebib  32624  fnpreimac  32749  fcnvgreu  32751  isoun  32781  fsuppcurry1  32803  fsuppcurry2  32804  prodpr  32907  prodtp  32908  pmtrprfv2  33170  elrgspnsubrunlem2  33330  nsgmgclem  33492  nsgqusf1olem2  33495  isprmidlc  33528  ssdifidllem  33537  ssdifidlprm  33539  ssmxidllem  33554  qsdrng  33578  1arithufdlem3  33627  ordtrest2NEWlem  34079  esumsplit  34210  esumpad2  34213  esumpcvgval  34235  sigaclcu2  34277  ldgenpisyslem1  34320  volmeas  34388  mbfmco2  34422  omsmeas  34480  oddpwdc  34511  eulerpartlemgvv  34533  ballotlemfc0  34650  ballotlemfcc  34651  prodfzo03  34760  circlemethhgt  34800  bnj1109  34942  bnj1294  34973  bnj545  35051  bnj605  35063  bnj594  35068  bnj934  35091  bnj953  35095  bnj1137  35151  bnj1174  35159  bnj1388  35189  subfacp1lem4  35377  erdszelem7  35391  erdszelem8  35392  erdsze2lem2  35398  resconn  35440  cvmsdisj  35464  cvmscld  35467  satf0op  35571  mclsax  35763  climuzcnv  35865  pocnv  35957  cgrid2  36197  btwncom  36208  btwnswapid2  36212  colinearperm1  36256  colinearperm3  36257  colinearperm2  36258  colinearperm4  36259  lineext  36270  colinbtwnle  36312  broutsideof2  36316  outsideofcom  36322  linecom  36344  linerflx2  36345  lineintmo  36351  fwddifn0  36358  hfext  36377  ntruni  36521  clsint2  36523  neibastop1  36553  weiunlem  36657  bj-snsetex  37164  relowlssretop  37568  pibt2  37622  fin2solem  37807  lindsadd  37814  matunitlindflem1  37817  poimirlem4  37825  poimirlem25  37846  poimirlem32  37853  opnmbllem0  37857  mblfinlem3  37860  mbfposadd  37868  itg2addnclem3  37874  ftc1anclem6  37899  ftc1anc  37902  ac6gf  37933  heibor1lem  38010  isdrngo2  38159  unichnidl  38232  isfldidl  38269  cnf1dd  38291  membpartlem19  39070  lkrss2N  39429  elpadd0  40069  ltrnu  40381  tendoex  41235  cdlemm10N  41378  dicfnN  41443  dihmeetlem2N  41559  dihlatat  41597  lcfrlem9  41810  uzindd  42231  sticksstones1  42400  ofun  42492  nn0addcom  42717  nn0mulcom  42721  zmulcomlem  42722  fsuppind  42833  prjspner1  42869  infdesc  42886  ismrcd1  42940  isnacs3  42952  pellfundglb  43127  jm2.22  43237  jm2.23  43238  isnumbasgrplem1  43343  hbtlem6  43371  rngunsnply  43411  ordsssucim  43644  mnringmulrcld  44469  dvgrat  44553  cvgdvgrat  44554  nznngen  44557  uzmptshftfval  44587  wfac8prim  45243  rnmptlb  45487  rnmptbddlem  45488  rnmptbd2lem  45492  iccshift  45764  iooshift  45768  liminflbuz2  46059  xlimbr  46071  itgperiod  46225  fourierdlem42  46393  fourierdlem68  46418  fourierdlem93  46443  smfpimne2  47084  elprneb  47275  dfatcolem  47501  modmknepk  47608  ichim  47703  ichnfb  47711  prproropf1olem1  47749  prproropf1olem3  47751  gpgnbgrvtx0  48320  gpgnbgrvtx1  48321  2zlidl  48486  lspsslco  48683  isthincd2  49682  fullthinc  49695