Theorem sylan2b 606

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syl2anb  610  eupickb  2665  2eu1  2680  2eu1v  2681  elnelne1  3077  elnelne2  3078  morex  3684  psssstr  4065  reuss2  4279  reupick  4282  reximdva0  4310  falseral0OLD  4478  rabsneu  4697  invdisjrab  5098  opabss  5177  triun  5235  triin  5237  poirr  5583  wefrc  5657  xpcan  6176  fnfco  6747  eqfnun  7036  fnressn  7159  fvtp3  7199  fvtp3g  7202  f1mpt  7261  offval  7689  ordsucuniel  7822  onzsl  7844  soex  7920  fiunlem  7941  fiun  7942  f1iun  7943  dfoprab3  8053  poxp  8126  fnwelem  8129  poxp2  8141  suppssr  8193  suppssrg  8194  suppsssn  8199  suppofssd  8201  fprlem2  8300  oeordsuc  8582  oelim2  8583  omsmolem  8645  ssnnfi  9157  ssfi  9160  ensymfib  9171  domnsymfi  9187  fiint  9289  unifi  9304  indexfi  9320  iinfi  9380  unwdomg  9549  inf3lem5  9604  rankr1bg  9778  rankr1c  9796  carden2a  9964  dfac8clem  10028  dfac5lem4  10122  pwsdompw  10198  cfsuc  10252  cflim2  10258  enfin2i  10316  isf34lem4  10372  axdc4lem  10450  zornn0g  10500  uniimadomf  10540  fpwwe2lem7  10633  fpwwe2lem11  10637  fpwwe2lem12  10638  pwfseqlem1  10654  pwfseqlem5  10659  intgru  10810  addclpi  10888  addnidpi  10897  ltsonq  10965  nqpr  11010  reclem3pr  11045  recexsr  11103  supsrlem  11107  nnnn0addcl  12545  un0addcl  12548  un0mulcl  12549  nn0nndivcl  12587  nn0ge0div  12676  uzind3  12701  uzind4  12941  zsupss  12972  rpnnen1lem2  13012  rpnnen1lem1  13013  rpnnen1lem3  13014  rpnnen1lem5  13016  ltsubrp  13065  ltaddrp  13066  xrlttr  13176  qbtwnxr  13237  xltnegi  13253  xaddnemnf  13273  xaddnepnf  13274  xaddcom  13277  xnegdi  13285  xsubge0  13298  xrub  13349  fzne1  13644  fzind2  13829  seqof  14108  expp1  14117  expneg  14118  expcllem  14121  mulexpz  14151  expaddz  14155  expmulz  14157  faclbnd4lem3  14344  faclbnd4  14346  fi1uzind  14557  swrd00  14697  swrd0  14713  cats1un  14775  reuccatpfxs1  14801  cshw0  14850  cshwn  14853  wwlktovfo  15014  shftf  15135  sqrtdiv  15335  leabs  15369  mulcn2  15666  summolem2  15785  fsumrev2  15851  geomulcvg  15948  prodmolem2  16007  zprod  16009  prodsn  16034  prodsnf  16036  fprodle  16068  bpolydiflem  16125  bpoly2  16128  bpoly3  16129  ruclem6  16308  dvdsflip  16392  dvdsfac  16401  gcdcllem1  16574  lcmgcdlem  16681  rpexp1i  16799  hashdvds  16851  hashgcdlem  16864  phisum  16867  iserodd  16912  pcqcl  16933  pcid  16950  ismred  17671  funcpropd  17976  natpropd  18053  odupos  18399  lubun  18588  rabsubmgmd  18783  sgrpidmnd  18818  issubmd  18887  grpinvnzcl  19100  mulgneg  19181  mulgnn0z  19190  symgfixf1  19530  symgsssg  19560  symgfisg  19561  pgpssslw  19707  sylow2alem2  19711  sylow2a  19712  oddvdssubg  19948  gsumzunsnd  20049  gsumunsnfd  20050  gsum2dlem1  20063  gsum2dlem2  20064  gsumcom3  20071  ablfac1eu  20168  pgpfac1lem5  20174  gsumdixp  20425  dvdsrcl2  20473  01eq0ring  20657  isdrng3lem1  20880  isdrng3lem2  20881  isdrngd  20897  isdrngdOLD  20899  unichnlidl  21391  isprmidlc  21501  ssdifidllem  21513  ssdifidlprm  21515  cnsubrg  21606  psgnodpm  21767  evlslem4  22256  psdmul  22358  coe1tmmul2  22466  mpomatmul  22632  cpmidpmat  23059  intcld  23226  neiptopnei  23318  ordtrest2lem  23389  lmss  23484  cmpcovf  23577  cncmp  23578  fincmp  23579  cmpsublem  23585  cmpsub  23586  unconn  23615  1stcfb  23631  2ndcsep  23645  refun0  23701  locfincmp  23712  1stckgenlem  23739  ptbasin  23763  ptbasfi  23767  ptunimpt  23781  ptuniconst  23784  dfac14  23804  ptcnp  23808  xkoptsub  23840  xkococnlem  23845  xkoinjcn  23873  qtopcmplem  23893  qtophmeo  24003  fbfinnfr  24027  isufil2  24094  isfcls  24195  xmetrtri  24541  xmetrtri2  24542  blssioo  24981  divcn  25056  bndth  25146  clmvscom  25278  resscdrg  25546  minveclem3  25617  finiunmbl  25732  opnmbllem  25789  ismbf2d  25828  itg2seq  25930  bddiblnc  26030  ellimc2  26065  limcmpt2  26072  limcres  26074  dvlem  26084  dvidlem  26103  dvrec  26143  dveflem  26167  dvlip  26181  coe1mul3  26285  dvtaylp  26562  leibpilem2  27135  leibpi  27136  wilthlem2  27262  basellem3  27276  dchreq  27451  dchrsum  27462  lgsval3  27508  lgsdir2lem4  27521  2sqlem6  27616  rpvmasumlem  27680  dchrisum0fno1  27704  rpvmasum2  27705  pntrsumbnd2  27760  ostthlem1  27820  nosupno  27896  negbdaylem  28278  expsp1  28651  colmid  28994  plngrotlem2  29099  lmiisolem  29134  dfcgra2  29170  prlngmolem2  29232  axcontlem2  29344  axcontlem7  29349  upgrex  29471  umgredg  29517  umgrpredgv  29519  umgredgne  29524  umgredgnlp  29526  usgredgppr  29575  edgssv2  29577  uspgredg2vlem  29602  usgredg2vlem1  29604  upgrres1  29692  nbuhgr2vtx1edgblem  29730  nbusgrf1o0  29748  hashnbusgrnn0  29755  iscplgredg  29796  uhgrvd00  29913  finsumvtxdg2size  29929  wlkepvtx  30037  wlknewwlksn  30265  wwlksnextfun  30276  wwlksnextsurj  30278  elwwlks2ons3im  30332  wwlks2onsym  30338  clwwlkf  30427  fusgreghash2wspv  30715  numclwwlk5lem  30767  grpoidinvlem3  30887  ablo32  30930  ablomuldiv  30933  ablodivdiv  30934  ablodiv32  30936  nvscom  31010  dipassr  31227  htthlem  31298  hsn0elch  31629  shscli  31698  nmopun  32395  branmfn  32486  mdslj1i  32700  mdslj2i  32701  atss  32727  chcv1  32736  dmdbr5ati  32803  snsssng  32889  ifnebib  32924  fnpreimac  33044  fcnvgreu  33046  isoun  33076  fsuppcurry1  33098  fsuppcurry2  33099  prodpr  33199  prodtp  33200  pmtrprfv2  33431  elrgspnsubrunlem2  33591  nsgmgclem  33743  nsgqusf1olem2  33746  ssmxidllem  33779  qsdrng  33802  1arithufdlem3  33859  ordtrest2NEWlem  34335  esumsplit  34466  esumpad2  34469  esumpcvgval  34491  sigaclcu2  34533  ldgenpisyslem1  34577  volmeas  34645  mbfmco2  34679  omsmeas  34737  oddpwdc  34768  eulerpartlemgvv  34790  ballotlemfc0  34907  ballotlemfcc  34908  prodfzo03  35014  circlemethhgt  35054  bnj1109  35199  bnj1294  35229  bnj545  35307  bnj605  35319  bnj594  35324  bnj934  35347  bnj953  35351  bnj1137  35407  bnj1174  35415  bnj1388  35445  vonf1oonfo  35615  subfacp1lem4  35688  erdszelem7  35702  erdszelem8  35703  erdsze2lem2  35709  resconn  35751  cvmsdisj  35775  cvmscld  35778  satf0op  35882  mclsax  36074  climuzcnv  36176  pocnv  36268  cgrid2  36508  btwncom  36519  btwnswapid2  36523  colinearperm1  36567  colinearperm3  36568  colinearperm2  36569  colinearperm4  36570  lineext  36581  colinbtwnle  36623  broutsideof2  36627  outsideofcom  36633  linecom  36655  linerflx2  36656  lineintmo  36662  fwddifn0  36669  hfext  36688  nmulel1  36720  ntruni  36871  clsint2  36873  neibastop1  36903  weiunlem  37007  bj-snsetex  37632  relowlssretop  38042  pibt2  38096  fin2solem  38290  lindsadd  38297  matunitlindflem1  38300  poimirlem4  38308  poimirlem25  38329  poimirlem32  38336  opnmbllem0  38340  mblfinlem3  38343  mbfposadd  38351  itg2addnclem3  38357  ftc1anclem6  38382  ftc1anc  38385  ac6gf  38416  heibor1lem  38493  isdrngo2  38642  unichnidl  38715  isfldidl  38752  cnf1dd  38772  membpartlem19  39596  lkrss2N  39976  elpadd0  40616  ltrnu  40928  tendoex  41782  cdlemm10N  41925  dicfnN  41990  dihmeetlem2N  42106  dihlatat  42144  lcfrlem9  42357  uzindd  42778  sticksstones1  42946  ofun  43039  nn0addcom  43269  nn0mulcom  43273  zmulcomlem  43274  fsuppind  43355  prjspner1  43391  infdesc  43408  ismrcd1  43462  isnacs3  43474  pellfundglb  43645  jm2.22  43755  jm2.23  43756  isnumbasgrplem1  43861  hbtlem6  43889  rngunsnply  43929  ordsssucim  44162  mnringmulrcld  44985  dvgrat  45055  cvgdvgrat  45056  nznngen  45059  uzmptshftfval  45089  wfac8prim  45744  rnmptlb  45991  rnmptbddlem  45992  rnmptbd2lem  45996  iccshift  46267  iooshift  46271  liminflbuz2  46562  xlimbr  46574  itgperiod  46728  fourierdlem42  46896  fourierdlem68  46921  fourierdlem93  46946  smfpimne2  47587  elprneb  47799  dfatcolem  48025  modmknepk  48138  ichim  48239  ichnfb  48247  prproropf1olem1  48285  prproropf1olem3  48287  gpgnbgrvtx0  48872  gpgnbgrvtx1  48873  2zlidl  49038  lspsslco  49250  isthincd2  50248  fullthinc  50261