Theorem sylan2b 603

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ 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 209  df-an 400

This theorem is referenced by:  syl2anb  607  eupickb  2661  2eu1  2676  2eu1v  2677  elnelne1  3071  elnelne2  3072  morex  3680  psssstr  4061  reuss2  4276  reupick  4279  reximdva0  4305  falseral0OLD  4466  rabsneu  4685  invdisjrab  5084  opabss  5161  triun  5219  triin  5221  poirr  5563  wefrc  5637  xpcan  6156  fnfco  6723  eqfnun  7012  fnressn  7135  fvtp3  7175  fvtp3g  7178  f1mpt  7239  offval  7663  ordsucuniel  7798  onzsl  7820  soex  7896  fiunlem  7917  fiun  7918  f1iun  7919  dfoprab3  8029  poxp  8101  fnwelem  8104  poxp2  8116  suppssr  8168  suppssrg  8169  suppsssn  8174  suppofssd  8176  fprlem2  8275  oeordsuc  8557  oelim2  8558  omsmolem  8620  ssnnfi  9131  ssfi  9134  ensymfib  9145  domnsymfi  9161  fiint  9264  unifi  9280  indexfi  9296  iinfi  9356  unwdomg  9525  inf3lem5  9580  rankr1bg  9754  rankr1c  9772  carden2a  9917  dfac8clem  9981  dfac5lem4  10075  dfac5lem4OLD  10077  pwsdompw  10152  cfsuc  10207  cflim2  10213  enfin2i  10271  isf34lem4  10327  axdc4lem  10405  zornn0g  10455  uniimadomf  10495  fpwwe2lem7  10588  fpwwe2lem11  10592  fpwwe2lem12  10593  pwfseqlem1  10609  pwfseqlem5  10614  intgru  10765  addclpi  10843  addnidpi  10852  ltsonq  10920  nqpr  10965  reclem3pr  11000  recexsr  11058  supsrlem  11062  nnnn0addcl  12504  un0addcl  12507  un0mulcl  12508  nn0nndivcl  12546  nn0ge0div  12635  uzind3  12660  uzind4  12900  zsupss  12931  rpnnen1lem2  12971  rpnnen1lem1  12972  rpnnen1lem3  12973  rpnnen1lem5  12975  ltsubrp  13024  ltaddrp  13025  xrlttr  13135  qbtwnxr  13196  xltnegi  13212  xaddnemnf  13232  xaddnepnf  13233  xaddcom  13236  xnegdi  13244  xsubge0  13257  xrub  13308  fzne1  13602  fzind2  13787  seqof  14065  expp1  14074  expneg  14075  expcllem  14078  mulexpz  14108  expaddz  14112  expmulz  14114  faclbnd4lem3  14301  faclbnd4  14303  fi1uzind  14513  swrd00  14651  swrd0  14665  cats1un  14727  reuccatpfxs1  14753  cshw0  14800  cshwn  14803  wwlktovfo  14964  shftf  15085  sqrtdiv  15282  leabs  15316  mulcn2  15613  summolem2  15733  fsumrev2  15799  geomulcvg  15896  prodmolem2  15955  zprod  15957  prodsn  15982  prodsnf  15984  fprodle  16016  bpolydiflem  16074  bpoly2  16077  bpoly3  16078  ruclem6  16257  dvdsflip  16341  dvdsfac  16350  gcdcllem1  16523  lcmgcdlem  16630  rpexp1i  16748  hashdvds  16800  hashgcdlem  16813  phisum  16816  iserodd  16861  pcqcl  16882  pcid  16899  ismred  17620  funcpropd  17925  natpropd  18002  odupos  18348  lubun  18537  rabsubmgmd  18728  sgrpidmnd  18763  issubmd  18830  grpinvnzcl  19043  mulgneg  19124  mulgnn0z  19133  symgfixf1  19467  symgsssg  19497  symgfisg  19498  pgpssslw  19644  sylow2alem2  19648  sylow2a  19649  oddvdssubg  19885  gsumzunsnd  19986  gsumunsnfd  19987  gsum2dlem1  20000  gsum2dlem2  20001  gsumcom3  20008  ablfac1eu  20105  pgpfac1lem5  20111  gsumdixp  20353  dvdsrcl2  20401  01eq0ring  20566  isdrngd  20801  isdrngdOLD  20803  cnsubrg  21466  psgnodpm  21627  evlslem4  22116  psdmul  22218  coe1tmmul2  22326  mpomatmul  22493  cpmidpmat  22920  intcld  23087  neiptopnei  23179  ordtrest2lem  23250  lmss  23345  cmpcovf  23438  cncmp  23439  fincmp  23440  cmpsublem  23446  cmpsub  23447  unconn  23476  1stcfb  23492  2ndcsep  23506  refun0  23562  locfincmp  23573  1stckgenlem  23600  ptbasin  23624  ptbasfi  23628  ptunimpt  23642  ptuniconst  23645  dfac14  23665  ptcnp  23669  xkoptsub  23701  xkococnlem  23706  xkoinjcn  23734  qtopcmplem  23754  qtophmeo  23864  fbfinnfr  23888  isufil2  23955  isfcls  24056  xmetrtri  24402  xmetrtri2  24403  blssioo  24842  divcn  24917  bndth  25007  clmvscom  25139  resscdrg  25407  minveclem3  25478  finiunmbl  25593  opnmbllem  25650  ismbf2d  25689  itg2seq  25791  bddiblnc  25891  ellimc2  25926  limcmpt2  25933  limcres  25935  dvlem  25945  dvidlem  25964  dvrec  26004  dveflem  26028  dvlip  26042  coe1mul3  26146  dvtaylp  26420  leibpilem2  26993  leibpi  26994  wilthlem2  27120  basellem3  27134  dchreq  27309  dchrsum  27320  lgsval3  27366  lgsdir2lem4  27379  2sqlem6  27474  rpvmasumlem  27538  dchrisum0fno1  27562  rpvmasum2  27563  pntrsumbnd2  27618  ostthlem1  27678  nosupno  27754  negbdaylem  28136  expsp1  28509  colmid  28844  lmiisolem  28952  dfcgra2  28986  axcontlem2  29122  axcontlem7  29127  upgrex  29249  umgredg  29295  umgrpredgv  29297  umgredgne  29302  umgredgnlp  29304  usgredgppr  29353  edgssv2  29355  uspgredg2vlem  29380  usgredg2vlem1  29382  upgrres1  29470  nbuhgr2vtx1edgblem  29508  nbusgrf1o0  29526  hashnbusgrnn0  29533  iscplgredg  29574  uhgrvd00  29691  finsumvtxdg2size  29707  wlkepvtx  29815  wlknewwlksn  30043  wwlksnextfun  30054  wwlksnextsurj  30056  elwwlks2ons3im  30110  wwlks2onsym  30116  clwwlkf  30205  fusgreghash2wspv  30493  numclwwlk5lem  30545  grpoidinvlem3  30665  ablo32  30708  ablomuldiv  30711  ablodivdiv  30712  ablodiv32  30714  nvscom  30788  dipassr  31005  htthlem  31076  hsn0elch  31407  shscli  31476  nmopun  32173  branmfn  32264  mdslj1i  32478  mdslj2i  32479  atss  32505  chcv1  32514  dmdbr5ati  32581  snsssng  32672  ifnebib  32707  fnpreimac  32832  fcnvgreu  32834  isoun  32864  fsuppcurry1  32886  fsuppcurry2  32887  prodpr  32988  prodtp  32989  pmtrprfv2  33228  elrgspnsubrunlem2  33389  nsgmgclem  33557  nsgqusf1olem2  33560  isprmidlc  33593  ssdifidllem  33603  ssdifidlprm  33605  ssmxidllem  33621  qsdrng  33645  1arithufdlem3  33702  ordtrest2NEWlem  34179  esumsplit  34310  esumpad2  34313  esumpcvgval  34335  sigaclcu2  34377  ldgenpisyslem1  34420  volmeas  34488  mbfmco2  34522  omsmeas  34580  oddpwdc  34611  eulerpartlemgvv  34633  ballotlemfc0  34750  ballotlemfcc  34751  prodfzo03  34857  circlemethhgt  34897  bnj1109  35042  bnj1294  35072  bnj545  35150  bnj605  35162  bnj594  35167  bnj934  35190  bnj953  35194  bnj1137  35250  bnj1174  35258  bnj1388  35288  vonf1oonfo  35418  subfacp1lem4  35493  erdszelem7  35507  erdszelem8  35508  erdsze2lem2  35514  resconn  35556  cvmsdisj  35580  cvmscld  35583  satf0op  35687  mclsax  35879  climuzcnv  35981  pocnv  36073  cgrid2  36313  btwncom  36324  btwnswapid2  36328  colinearperm1  36372  colinearperm3  36373  colinearperm2  36374  colinearperm4  36375  lineext  36386  colinbtwnle  36428  broutsideof2  36432  outsideofcom  36438  linecom  36460  linerflx2  36461  lineintmo  36467  fwddifn0  36474  hfext  36493  ntruni  36647  clsint2  36649  neibastop1  36679  weiunlem  36783  bj-snsetex  37408  relowlssretop  37817  pibt2  37871  fin2solem  38065  lindsadd  38072  matunitlindflem1  38075  poimirlem4  38083  poimirlem25  38104  poimirlem32  38111  opnmbllem0  38115  mblfinlem3  38118  mbfposadd  38126  itg2addnclem3  38132  ftc1anclem6  38157  ftc1anc  38160  ac6gf  38191  heibor1lem  38268  isdrngo2  38417  unichnidl  38490  isfldidl  38527  cnf1dd  38549  membpartlem19  39373  lkrss2N  39753  elpadd0  40393  ltrnu  40705  tendoex  41559  cdlemm10N  41702  dicfnN  41767  dihmeetlem2N  41883  dihlatat  41921  lcfrlem9  42134  uzindd  42555  sticksstones1  42723  ofun  42814  nn0addcom  43044  nn0mulcom  43048  zmulcomlem  43049  fsuppind  43132  prjspner1  43168  infdesc  43185  ismrcd1  43239  isnacs3  43251  pellfundglb  43422  jm2.22  43532  jm2.23  43533  isnumbasgrplem1  43638  hbtlem6  43666  rngunsnply  43706  ordsssucim  43939  mnringmulrcld  44764  dvgrat  44848  cvgdvgrat  44849  nznngen  44852  uzmptshftfval  44882  wfac8prim  45538  rnmptlb  45778  rnmptbddlem  45779  rnmptbd2lem  45783  iccshift  46054  iooshift  46058  liminflbuz2  46349  xlimbr  46361  itgperiod  46515  fourierdlem42  46683  fourierdlem68  46708  fourierdlem93  46733  smfpimne2  47374  elprneb  47583  dfatcolem  47809  modmknepk  47922  ichim  48023  ichnfb  48031  prproropf1olem1  48069  prproropf1olem3  48071  gpgnbgrvtx0  48656  gpgnbgrvtx1  48657  2zlidl  48822  lspsslco  49019  isthincd2  50018  fullthinc  50031