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  2632  2eu1  2648  2eu1v  2649  eqtr3OLD  2761  elnelne1  3054  elnelne2  3055  morex  3727  psssstr  4118  reuss2  4331  reupick  4334  reximdva0  4360  falseral0  4521  rabsneu  4733  invdisjrab  5134  opabss  5211  triun  5279  triin  5281  poirr  5608  wefrc  5682  xpcan  6197  fnfco  6773  eqfnun  7056  fnressn  7177  fvtp3  7216  fvtp3g  7219  f1mpt  7280  offval  7705  ordsucuniel  7843  onzsl  7866  soex  7943  fiunlem  7964  fiun  7965  f1iun  7966  dfoprab3  8077  poxp  8151  fnwelem  8154  poxp2  8166  suppssr  8218  suppssrg  8219  suppsssn  8224  suppofssd  8226  fprlem2  8324  oeordsuc  8630  oelim2  8631  omsmolem  8693  rexdif1enOLD  9197  ssnnfi  9207  ssfi  9211  ensymfib  9221  domnsymfi  9237  fiint  9363  fiintOLD  9364  unifi  9381  indexfi  9397  iinfi  9454  unwdomg  9621  inf3lem5  9669  rankr1bg  9840  rankr1c  9858  carden2a  10003  dfac8clem  10069  dfac5lem4  10163  dfac5lem4OLD  10165  pwsdompw  10240  cfsuc  10294  cflim2  10300  enfin2i  10358  isf34lem4  10414  axdc4lem  10492  zornn0g  10542  uniimadomf  10582  fpwwe2lem7  10674  fpwwe2lem11  10678  fpwwe2lem12  10679  pwfseqlem1  10695  pwfseqlem5  10700  intgru  10851  addclpi  10929  addnidpi  10938  ltsonq  11006  nqpr  11051  reclem3pr  11086  recexsr  11144  supsrlem  11148  nnnn0addcl  12553  un0addcl  12556  un0mulcl  12557  nn0nndivcl  12595  nn0ge0div  12684  uzind3  12709  uzind4  12945  zsupss  12976  rpnnen1lem2  13016  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem5  13020  ltsubrp  13068  ltaddrp  13069  xrlttr  13178  qbtwnxr  13238  xltnegi  13254  xaddnemnf  13274  xaddnepnf  13275  xaddcom  13278  xnegdi  13286  xsubge0  13299  xrub  13350  fzne1  13640  fzind2  13820  seqof  14096  expp1  14105  expneg  14106  expcllem  14109  mulexpz  14139  expaddz  14143  expmulz  14145  faclbnd4lem3  14330  faclbnd4  14332  fi1uzind  14542  swrd00  14678  swrd0  14692  cats1un  14755  reuccatpfxs1  14781  cshw0  14828  cshwn  14831  wwlktovfo  14993  shftf  15114  sqrtdiv  15300  leabs  15334  mulcn2  15628  summolem2  15748  fsumrev2  15814  geomulcvg  15908  prodmolem2  15967  zprod  15969  prodsn  15994  prodsnf  15996  fprodle  16028  bpolydiflem  16086  bpoly2  16089  bpoly3  16090  ruclem6  16267  dvdsflip  16350  dvdsfac  16359  gcdcllem1  16532  lcmgcdlem  16639  rpexp1i  16756  hashdvds  16808  hashgcdlem  16821  phisum  16823  iserodd  16868  pcqcl  16889  pcid  16906  ismred  17646  funcpropd  17953  natpropd  18032  odupos  18385  lubun  18572  rabsubmgmd  18729  sgrpidmnd  18764  issubmd  18831  grpinvnzcl  19041  mulgneg  19122  mulgnn0z  19131  symgfixf1  19469  symgsssg  19499  symgfisg  19500  pgpssslw  19646  sylow2alem2  19650  sylow2a  19651  oddvdssubg  19887  gsumzunsnd  19988  gsumunsnfd  19989  gsum2dlem1  20002  gsum2dlem2  20003  gsumcom3  20010  ablfac1eu  20107  pgpfac1lem5  20113  gsumdixp  20332  dvdsrcl2  20382  01eq0ring  20546  isdrngd  20781  isdrngdOLD  20783  cnsubrg  21462  psgnodpm  21623  evlslem4  22117  psdmul  22187  coe1tmmul2  22294  mpomatmul  22467  cpmidpmat  22894  intcld  23063  neiptopnei  23155  ordtrest2lem  23226  lmss  23321  cmpcovf  23414  cncmp  23415  fincmp  23416  cmpsublem  23422  cmpsub  23423  unconn  23452  1stcfb  23468  2ndcsep  23482  refun0  23538  locfincmp  23549  1stckgenlem  23576  ptbasin  23600  ptbasfi  23604  ptunimpt  23618  ptuniconst  23621  dfac14  23641  ptcnp  23645  xkoptsub  23677  xkococnlem  23682  xkoinjcn  23710  qtopcmplem  23730  qtophmeo  23840  fbfinnfr  23864  isufil2  23931  isfcls  24032  xmetrtri  24380  xmetrtri2  24381  blssioo  24830  divcnOLD  24903  divcn  24905  bndth  25003  clmvscom  25136  resscdrg  25405  minveclem3  25476  finiunmbl  25592  opnmbllem  25649  ismbf2d  25688  itg2seq  25791  bddiblnc  25891  ellimc2  25926  limcmpt2  25933  limcres  25935  dvlem  25945  dvidlem  25964  dvrec  26007  dveflem  26031  dvlip  26046  coe1mul3  26152  dvtaylp  26426  leibpilem2  26998  leibpi  26999  wilthlem2  27126  basellem3  27140  dchreq  27316  dchrsum  27327  lgsval3  27373  lgsdir2lem4  27386  2sqlem6  27481  rpvmasumlem  27545  dchrisum0fno1  27569  rpvmasum2  27570  pntrsumbnd2  27625  ostthlem1  27685  nosupno  27762  negsbdaylem  28102  expsp1  28426  colmid  28710  lmiisolem  28818  dfcgra2  28852  axcontlem2  28994  axcontlem7  28999  upgrex  29123  umgredg  29169  umgrpredgv  29171  umgredgne  29176  umgredgnlp  29178  usgredgppr  29227  edgssv2  29229  uspgredg2vlem  29254  usgredg2vlem1  29256  upgrres1  29344  nbuhgr2vtx1edgblem  29382  nbusgrf1o0  29400  hashnbusgrnn0  29407  iscplgredg  29448  uhgrvd00  29566  finsumvtxdg2size  29582  wlkepvtx  29692  wlknewwlksn  29916  wwlksnextfun  29927  wwlksnextsurj  29929  elwwlks2ons3im  29983  wwlks2onsym  29987  clwwlkf  30075  fusgreghash2wspv  30363  numclwwlk5lem  30415  grpoidinvlem3  30534  ablo32  30577  ablomuldiv  30580  ablodivdiv  30581  ablodiv32  30583  nvscom  30657  dipassr  30874  htthlem  30945  hsn0elch  31276  shscli  31345  nmopun  32042  branmfn  32133  mdslj1i  32347  mdslj2i  32348  atss  32374  chcv1  32383  dmdbr5ati  32450  snsssng  32541  ifnebib  32569  fnpreimac  32687  fcnvgreu  32689  isoun  32716  fsuppcurry1  32742  fsuppcurry2  32743  prodpr  32832  prodtp  32833  pmtrprfv2  33090  nsgmgclem  33418  nsgqusf1olem2  33421  isprmidlc  33454  ssdifidllem  33463  ssdifidlprm  33465  ssmxidllem  33480  qsdrng  33504  1arithufdlem3  33553  ordtrest2NEWlem  33882  esumsplit  34033  esumpad2  34036  esumpcvgval  34058  sigaclcu2  34100  ldgenpisyslem1  34143  volmeas  34211  mbfmco2  34246  omsmeas  34304  oddpwdc  34335  eulerpartlemgvv  34357  ballotlemfc0  34473  ballotlemfcc  34474  prodfzo03  34596  circlemethhgt  34636  bnj1109  34778  bnj1294  34809  bnj545  34887  bnj605  34899  bnj594  34904  bnj934  34927  bnj953  34931  bnj1137  34987  bnj1174  34995  bnj1388  35025  subfacp1lem4  35167  erdszelem7  35181  erdszelem8  35182  erdsze2lem2  35188  resconn  35230  cvmsdisj  35254  cvmscld  35257  satf0op  35361  mclsax  35553  climuzcnv  35655  pocnv  35742  cgrid2  35984  btwncom  35995  btwnswapid2  35999  colinearperm1  36043  colinearperm3  36044  colinearperm2  36045  colinearperm4  36046  lineext  36057  colinbtwnle  36099  broutsideof2  36103  outsideofcom  36109  linecom  36131  linerflx2  36132  lineintmo  36138  fwddifn0  36145  hfext  36164  ntruni  36309  clsint2  36311  neibastop1  36341  weiunlem2  36445  bj-snsetex  36945  relowlssretop  37345  pibt2  37399  fin2solem  37592  lindsadd  37599  matunitlindflem1  37602  poimirlem4  37610  poimirlem25  37631  poimirlem32  37638  opnmbllem0  37642  mblfinlem3  37645  mbfposadd  37653  itg2addnclem3  37659  ftc1anclem6  37684  ftc1anc  37687  ac6gf  37718  heibor1lem  37795  isdrngo2  37944  unichnidl  38017  isfldidl  38054  cnf1dd  38076  membpartlem19  38792  lkrss2N  39150  elpadd0  39791  ltrnu  40103  tendoex  40957  cdlemm10N  41100  dicfnN  41165  dihmeetlem2N  41281  dihlatat  41319  lcfrlem9  41532  uzindd  41958  sticksstones1  42127  metakunt12  42197  ofun  42255  nn0addcom  42456  nn0mulcom  42460  zmulcomlem  42461  fsuppind  42576  prjspner1  42612  infdesc  42629  ismrcd1  42685  isnacs3  42697  pellfundglb  42872  jm2.22  42983  jm2.23  42984  isnumbasgrplem1  43089  hbtlem6  43117  rngunsnply  43157  ordsssucim  43391  mnringmulrcld  44223  dvgrat  44307  cvgdvgrat  44308  nznngen  44311  uzmptshftfval  44341  rnmptlb  45187  rnmptbddlem  45188  rnmptbd2lem  45192  iccshift  45470  iooshift  45474  liminflbuz2  45770  xlimbr  45782  itgperiod  45936  fourierdlem42  46104  fourierdlem68  46129  fourierdlem93  46154  smfpimne2  46795  elprneb  46978  dfatcolem  47204  ichim  47381  ichnfb  47389  prproropf1olem1  47427  prproropf1olem3  47429  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  2zlidl  48083  lspsslco  48282  isthincd2  48837  fullthinc  48845