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  3048  elnelne2  3049  morex  3707  psssstr  4089  reuss2  4306  reupick  4309  reximdva0  4335  falseral0  4496  rabsneu  4710  invdisjrab  5111  opabss  5188  triun  5249  triin  5251  poirr  5578  wefrc  5653  xpcan  6170  fnfco  6748  eqfnun  7032  fnressn  7153  fvtp3  7194  fvtp3g  7197  f1mpt  7259  offval  7685  ordsucuniel  7823  onzsl  7846  soex  7922  fiunlem  7945  fiun  7946  f1iun  7947  dfoprab3  8058  poxp  8132  fnwelem  8135  poxp2  8147  suppssr  8199  suppssrg  8200  suppsssn  8205  suppofssd  8207  fprlem2  8305  oeordsuc  8611  oelim2  8612  omsmolem  8674  rexdif1enOLD  9178  ssnnfi  9188  ssfi  9192  ensymfib  9203  domnsymfi  9219  fiint  9343  fiintOLD  9344  unifi  9361  indexfi  9377  iinfi  9434  unwdomg  9603  inf3lem5  9651  rankr1bg  9822  rankr1c  9840  carden2a  9985  dfac8clem  10051  dfac5lem4  10145  dfac5lem4OLD  10147  pwsdompw  10222  cfsuc  10276  cflim2  10282  enfin2i  10340  isf34lem4  10396  axdc4lem  10474  zornn0g  10524  uniimadomf  10564  fpwwe2lem7  10656  fpwwe2lem11  10660  fpwwe2lem12  10661  pwfseqlem1  10677  pwfseqlem5  10682  intgru  10833  addclpi  10911  addnidpi  10920  ltsonq  10988  nqpr  11033  reclem3pr  11068  recexsr  11126  supsrlem  11130  nnnn0addcl  12536  un0addcl  12539  un0mulcl  12540  nn0nndivcl  12578  nn0ge0div  12667  uzind3  12692  uzind4  12927  zsupss  12958  rpnnen1lem2  12998  rpnnen1lem1  12999  rpnnen1lem3  13000  rpnnen1lem5  13002  ltsubrp  13050  ltaddrp  13051  xrlttr  13161  qbtwnxr  13221  xltnegi  13237  xaddnemnf  13257  xaddnepnf  13258  xaddcom  13261  xnegdi  13269  xsubge0  13282  xrub  13333  fzne1  13626  fzind2  13806  seqof  14082  expp1  14091  expneg  14092  expcllem  14095  mulexpz  14125  expaddz  14129  expmulz  14131  faclbnd4lem3  14318  faclbnd4  14320  fi1uzind  14530  swrd00  14667  swrd0  14681  cats1un  14744  reuccatpfxs1  14770  cshw0  14817  cshwn  14820  wwlktovfo  14982  shftf  15103  sqrtdiv  15289  leabs  15323  mulcn2  15617  summolem2  15737  fsumrev2  15803  geomulcvg  15897  prodmolem2  15956  zprod  15958  prodsn  15983  prodsnf  15985  fprodle  16017  bpolydiflem  16075  bpoly2  16078  bpoly3  16079  ruclem6  16258  dvdsflip  16341  dvdsfac  16350  gcdcllem1  16523  lcmgcdlem  16630  rpexp1i  16747  hashdvds  16799  hashgcdlem  16812  phisum  16815  iserodd  16860  pcqcl  16881  pcid  16898  ismred  17619  funcpropd  17920  natpropd  17997  odupos  18343  lubun  18530  rabsubmgmd  18687  sgrpidmnd  18722  issubmd  18789  grpinvnzcl  18999  mulgneg  19080  mulgnn0z  19089  symgfixf1  19423  symgsssg  19453  symgfisg  19454  pgpssslw  19600  sylow2alem2  19604  sylow2a  19605  oddvdssubg  19841  gsumzunsnd  19942  gsumunsnfd  19943  gsum2dlem1  19956  gsum2dlem2  19957  gsumcom3  19964  ablfac1eu  20061  pgpfac1lem5  20067  gsumdixp  20284  dvdsrcl2  20331  01eq0ring  20495  isdrngd  20730  isdrngdOLD  20732  cnsubrg  21400  psgnodpm  21553  evlslem4  22039  psdmul  22109  coe1tmmul2  22218  mpomatmul  22389  cpmidpmat  22816  intcld  22983  neiptopnei  23075  ordtrest2lem  23146  lmss  23241  cmpcovf  23334  cncmp  23335  fincmp  23336  cmpsublem  23342  cmpsub  23343  unconn  23372  1stcfb  23388  2ndcsep  23402  refun0  23458  locfincmp  23469  1stckgenlem  23496  ptbasin  23520  ptbasfi  23524  ptunimpt  23538  ptuniconst  23541  dfac14  23561  ptcnp  23565  xkoptsub  23597  xkococnlem  23602  xkoinjcn  23630  qtopcmplem  23650  qtophmeo  23760  fbfinnfr  23784  isufil2  23851  isfcls  23952  xmetrtri  24299  xmetrtri2  24300  blssioo  24739  divcnOLD  24813  divcn  24815  bndth  24913  clmvscom  25046  resscdrg  25315  minveclem3  25386  finiunmbl  25502  opnmbllem  25559  ismbf2d  25598  itg2seq  25700  bddiblnc  25800  ellimc2  25835  limcmpt2  25842  limcres  25844  dvlem  25854  dvidlem  25873  dvrec  25916  dveflem  25940  dvlip  25955  coe1mul3  26061  dvtaylp  26335  leibpilem2  26908  leibpi  26909  wilthlem2  27036  basellem3  27050  dchreq  27226  dchrsum  27237  lgsval3  27283  lgsdir2lem4  27296  2sqlem6  27391  rpvmasumlem  27455  dchrisum0fno1  27479  rpvmasum2  27480  pntrsumbnd2  27535  ostthlem1  27595  nosupno  27672  negsbdaylem  28019  expsp1  28372  colmid  28672  lmiisolem  28780  dfcgra2  28814  axcontlem2  28949  axcontlem7  28954  upgrex  29076  umgredg  29122  umgrpredgv  29124  umgredgne  29129  umgredgnlp  29131  usgredgppr  29180  edgssv2  29182  uspgredg2vlem  29207  usgredg2vlem1  29209  upgrres1  29297  nbuhgr2vtx1edgblem  29335  nbusgrf1o0  29353  hashnbusgrnn0  29360  iscplgredg  29401  uhgrvd00  29519  finsumvtxdg2size  29535  wlkepvtx  29645  wlknewwlksn  29874  wwlksnextfun  29885  wwlksnextsurj  29887  elwwlks2ons3im  29941  wwlks2onsym  29945  clwwlkf  30033  fusgreghash2wspv  30321  numclwwlk5lem  30373  grpoidinvlem3  30492  ablo32  30535  ablomuldiv  30538  ablodivdiv  30539  ablodiv32  30541  nvscom  30615  dipassr  30832  htthlem  30903  hsn0elch  31234  shscli  31303  nmopun  32000  branmfn  32091  mdslj1i  32305  mdslj2i  32306  atss  32332  chcv1  32341  dmdbr5ati  32408  snsssng  32500  ifnebib  32535  fnpreimac  32654  fcnvgreu  32656  isoun  32684  fsuppcurry1  32707  fsuppcurry2  32708  prodpr  32810  prodtp  32811  pmtrprfv2  33104  elrgspnsubrunlem2  33248  nsgmgclem  33431  nsgqusf1olem2  33434  isprmidlc  33467  ssdifidllem  33476  ssdifidlprm  33478  ssmxidllem  33493  qsdrng  33517  1arithufdlem3  33566  ordtrest2NEWlem  33958  esumsplit  34089  esumpad2  34092  esumpcvgval  34114  sigaclcu2  34156  ldgenpisyslem1  34199  volmeas  34267  mbfmco2  34302  omsmeas  34360  oddpwdc  34391  eulerpartlemgvv  34413  ballotlemfc0  34530  ballotlemfcc  34531  prodfzo03  34640  circlemethhgt  34680  bnj1109  34822  bnj1294  34853  bnj545  34931  bnj605  34943  bnj594  34948  bnj934  34971  bnj953  34975  bnj1137  35031  bnj1174  35039  bnj1388  35069  subfacp1lem4  35210  erdszelem7  35224  erdszelem8  35225  erdsze2lem2  35231  resconn  35273  cvmsdisj  35297  cvmscld  35300  satf0op  35404  mclsax  35596  climuzcnv  35698  pocnv  35785  cgrid2  36026  btwncom  36037  btwnswapid2  36041  colinearperm1  36085  colinearperm3  36086  colinearperm2  36087  colinearperm4  36088  lineext  36099  colinbtwnle  36141  broutsideof2  36145  outsideofcom  36151  linecom  36173  linerflx2  36174  lineintmo  36180  fwddifn0  36187  hfext  36206  ntruni  36350  clsint2  36352  neibastop1  36382  weiunlem2  36486  bj-snsetex  36986  relowlssretop  37386  pibt2  37440  fin2solem  37635  lindsadd  37642  matunitlindflem1  37645  poimirlem4  37653  poimirlem25  37674  poimirlem32  37681  opnmbllem0  37685  mblfinlem3  37688  mbfposadd  37696  itg2addnclem3  37702  ftc1anclem6  37727  ftc1anc  37730  ac6gf  37761  heibor1lem  37838  isdrngo2  37987  unichnidl  38060  isfldidl  38097  cnf1dd  38119  membpartlem19  38834  lkrss2N  39192  elpadd0  39833  ltrnu  40145  tendoex  40999  cdlemm10N  41142  dicfnN  41207  dihmeetlem2N  41323  dihlatat  41361  lcfrlem9  41574  uzindd  41995  sticksstones1  42164  ofun  42254  nn0addcom  42468  nn0mulcom  42472  zmulcomlem  42473  fsuppind  42588  prjspner1  42624  infdesc  42641  ismrcd1  42696  isnacs3  42708  pellfundglb  42883  jm2.22  42994  jm2.23  42995  isnumbasgrplem1  43100  hbtlem6  43128  rngunsnply  43168  ordsssucim  43401  mnringmulrcld  44227  dvgrat  44311  cvgdvgrat  44312  nznngen  44315  uzmptshftfval  44345  wfac8prim  45002  rnmptlb  45247  rnmptbddlem  45248  rnmptbd2lem  45252  iccshift  45527  iooshift  45531  liminflbuz2  45824  xlimbr  45836  itgperiod  45990  fourierdlem42  46158  fourierdlem68  46183  fourierdlem93  46208  smfpimne2  46849  elprneb  47038  dfatcolem  47264  ichim  47451  ichnfb  47459  prproropf1olem1  47497  prproropf1olem3  47499  gpgnbgrvtx0  48056  gpgnbgrvtx1  48057  2zlidl  48195  lspsslco  48393  isthincd2  49303  fullthinc  49316