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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  syl2anb  598  eupickb  2631  2eu1  2646  2eu1v  2647  eqtr3OLD  2759  elnelne1  3057  elnelne2  3058  morex  3714  psssstr  4105  reuss2  4314  reupick  4317  reximdva0  4350  falseral0  4518  rabsneu  4732  invdisjrabw  5132  opabss  5211  triun  5279  triin  5281  poirr  5599  wefrc  5669  xpcan  6172  fnfco  6753  eqfnun  7035  fnressn  7152  fvtp3  7194  fvtp3g  7197  f1mpt  7256  offval  7675  ordsucuniel  7808  onzsl  7831  soex  7908  fiunlem  7924  fiun  7925  f1iun  7926  dfoprab3  8036  poxp  8110  fnwelem  8113  poxp2  8125  suppssr  8177  suppssrg  8178  suppsssn  8182  suppofssd  8184  fprlem2  8282  oeordsuc  8590  oelim2  8591  omsmolem  8652  rexdif1enOLD  9155  ssnnfi  9165  ssnnfiOLD  9166  ssfi  9169  ensymfib  9183  domnsymfi  9199  fiint  9320  unifi  9337  indexfi  9356  iinfi  9408  unwdomg  9575  inf3lem5  9623  rankr1bg  9794  rankr1c  9812  carden2a  9957  dfac8clem  10023  dfac5lem4  10117  pwsdompw  10195  cfsuc  10248  cflim2  10254  enfin2i  10312  isf34lem4  10368  axdc4lem  10446  zornn0g  10496  uniimadomf  10536  fpwwe2lem7  10628  fpwwe2lem11  10632  fpwwe2lem12  10633  pwfseqlem1  10649  pwfseqlem5  10654  intgru  10805  addclpi  10883  addnidpi  10892  ltsonq  10960  nqpr  11005  reclem3pr  11040  recexsr  11098  supsrlem  11102  nnnn0addcl  12498  un0addcl  12501  un0mulcl  12502  nn0nndivcl  12539  nn0ge0div  12627  uzind3  12652  uzind4  12886  zsupss  12917  rpnnen1lem2  12957  rpnnen1lem1  12958  rpnnen1lem3  12959  rpnnen1lem5  12961  ltsubrp  13006  ltaddrp  13007  xrlttr  13115  qbtwnxr  13175  xltnegi  13191  xaddnemnf  13211  xaddnepnf  13212  xaddcom  13215  xnegdi  13223  xsubge0  13236  xrub  13287  fzind2  13746  seqof  14021  expp1  14030  expneg  14031  expcllem  14034  mulexpz  14064  expaddz  14068  expmulz  14070  faclbnd4lem3  14251  faclbnd4  14253  fi1uzind  14454  swrd00  14590  swrd0  14604  cats1un  14667  reuccatpfxs1  14693  cshw0  14740  cshwn  14743  wwlktovfo  14905  shftf  15022  sqrtdiv  15208  leabs  15242  mulcn2  15536  summolem2  15658  fsumrev2  15724  geomulcvg  15818  prodmolem2  15875  zprod  15877  prodsn  15902  prodsnf  15904  fprodle  15936  bpolydiflem  15994  bpoly2  15997  bpoly3  15998  ruclem6  16174  dvdsflip  16256  dvdsfac  16265  gcdcllem1  16436  lcmgcdlem  16539  rpexp1i  16656  hashdvds  16704  hashgcdlem  16717  phisum  16719  iserodd  16764  pcqcl  16785  pcid  16802  ismred  17542  funcpropd  17847  natpropd  17925  odupos  18277  lubun  18464  sgrpidmnd  18626  issubmd  18683  grpinvnzcl  18891  mulgneg  18966  mulgnn0z  18975  symgfixf1  19299  symgsssg  19329  symgfisg  19330  pgpssslw  19476  sylow2alem2  19480  sylow2a  19481  oddvdssubg  19717  gsumzunsnd  19818  gsumunsnfd  19819  gsum2dlem1  19832  gsum2dlem2  19833  gsumcom3  19840  ablfac1eu  19937  pgpfac1lem5  19943  gsumdixp  20124  dvdsrcl2  20172  01eq0ring  20297  isdrngd  20340  isdrngdOLD  20342  cnsubrg  20997  psgnodpm  21132  evlslem4  21628  coe1tmmul2  21789  mpomatmul  21939  cpmidpmat  22366  intcld  22535  neiptopnei  22627  ordtrest2lem  22698  lmss  22793  cmpcovf  22886  cncmp  22887  fincmp  22888  cmpsublem  22894  cmpsub  22895  unconn  22924  1stcfb  22940  2ndcsep  22954  refun0  23010  locfincmp  23021  1stckgenlem  23048  ptbasin  23072  ptbasfi  23076  ptunimpt  23090  ptuniconst  23093  dfac14  23113  ptcnp  23117  xkoptsub  23149  xkococnlem  23154  xkoinjcn  23182  qtopcmplem  23202  qtophmeo  23312  fbfinnfr  23336  isufil2  23403  isfcls  23504  xmetrtri  23852  xmetrtri2  23853  blssioo  24302  divcn  24375  bndth  24465  clmvscom  24597  resscdrg  24866  minveclem3  24937  finiunmbl  25052  opnmbllem  25109  ismbf2d  25148  itg2seq  25251  bddiblnc  25350  ellimc2  25385  limcmpt2  25392  limcres  25394  dvlem  25404  dvidlem  25423  dvrec  25463  dveflem  25487  dvlip  25501  coe1mul3  25608  dvtaylp  25873  leibpilem2  26435  leibpi  26436  wilthlem2  26562  basellem3  26576  dchreq  26750  dchrsum  26761  lgsval3  26807  lgsdir2lem4  26820  2sqlem6  26915  rpvmasumlem  26979  dchrisum0fno1  27003  rpvmasum2  27004  pntrsumbnd2  27059  ostthlem1  27119  nosupno  27195  negsbdaylem  27519  colmid  27928  lmiisolem  28036  dfcgra2  28070  axcontlem2  28212  axcontlem7  28217  upgrex  28341  umgredg  28387  umgrpredgv  28389  umgredgne  28394  umgredgnlp  28396  usgredgppr  28442  edgssv2  28444  uspgredg2vlem  28469  usgredg2vlem1  28471  upgrres1  28559  nbuhgr2vtx1edgblem  28597  nbusgrf1o0  28615  hashnbusgrnn0  28622  iscplgredg  28663  uhgrvd00  28780  finsumvtxdg2size  28796  wlkepvtx  28906  wlknewwlksn  29130  wwlksnextfun  29141  wwlksnextsurj  29143  elwwlks2ons3im  29197  wwlks2onsym  29201  clwwlkf  29289  fusgreghash2wspv  29577  numclwwlk5lem  29629  grpoidinvlem3  29746  ablo32  29789  ablomuldiv  29792  ablodivdiv  29793  ablodiv32  29795  nvscom  29869  dipassr  30086  htthlem  30157  hsn0elch  30488  shscli  30557  nmopun  31254  branmfn  31345  mdslj1i  31559  mdslj2i  31560  atss  31586  chcv1  31595  dmdbr5ati  31662  snsssng  31739  ifnebib  31768  fnpreimac  31883  fcnvgreu  31885  isoun  31910  fsuppcurry1  31937  fsuppcurry2  31938  fzne1  31986  prodpr  32019  prodtp  32020  pmtrprfv2  32236  nsgmgclem  32510  nsgqusf1olem2  32513  isprmidlc  32554  ssmxidllem  32577  qsdrng  32599  ordtrest2NEWlem  32890  esumsplit  33039  esumpad2  33042  esumpcvgval  33064  sigaclcu2  33106  ldgenpisyslem1  33149  volmeas  33217  mbfmco2  33252  omsmeas  33310  oddpwdc  33341  eulerpartlemgvv  33363  ballotlemfc0  33479  ballotlemfcc  33480  prodfzo03  33603  circlemethhgt  33643  bnj1109  33785  bnj1294  33816  bnj545  33894  bnj605  33906  bnj594  33911  bnj934  33934  bnj953  33938  bnj1137  33994  bnj1174  34002  bnj1388  34032  subfacp1lem4  34162  erdszelem7  34176  erdszelem8  34177  erdsze2lem2  34183  resconn  34225  cvmsdisj  34249  cvmscld  34252  satf0op  34356  mclsax  34548  climuzcnv  34644  pocnv  34721  cgrid2  34963  btwncom  34974  btwnswapid2  34978  colinearperm1  35022  colinearperm3  35023  colinearperm2  35024  colinearperm4  35025  lineext  35036  colinbtwnle  35078  broutsideof2  35082  outsideofcom  35088  linecom  35110  linerflx2  35111  lineintmo  35117  fwddifn0  35124  hfext  35143  gg-divcn  35151  ntruni  35200  clsint2  35202  neibastop1  35232  bj-snsetex  35832  relowlssretop  36232  pibt2  36286  fin2solem  36462  lindsadd  36469  matunitlindflem1  36472  poimirlem4  36480  poimirlem25  36501  poimirlem32  36508  opnmbllem0  36512  mblfinlem3  36515  mbfposadd  36523  itg2addnclem3  36529  ftc1anclem6  36554  ftc1anc  36557  ac6gf  36588  heibor1lem  36665  isdrngo2  36814  unichnidl  36887  isfldidl  36924  cnf1dd  36946  membpartlem19  37669  lkrss2N  38027  elpadd0  38668  ltrnu  38980  tendoex  39834  cdlemm10N  39977  dicfnN  40042  dihmeetlem2N  40158  dihlatat  40196  lcfrlem9  40409  uzindd  40830  sticksstones1  40950  metakunt12  40984  ofun  41055  fsuppind  41159  nn0addcom  41319  nn0mulcom  41323  zmulcomlem  41324  prjspner1  41364  infdesc  41381  ismrcd1  41421  isnacs3  41433  pellfundglb  41608  jm2.22  41719  jm2.23  41720  isnumbasgrplem1  41828  hbtlem6  41856  rngunsnply  41900  ordsssucim  42138  mnringmulrcld  42972  dvgrat  43056  cvgdvgrat  43057  nznngen  43060  uzmptshftfval  43090  rnmptlb  43932  rnmptbddlem  43933  rnmptbd2lem  43938  iccshift  44217  iooshift  44221  liminflbuz2  44517  xlimbr  44529  itgperiod  44683  fourierdlem42  44851  fourierdlem68  44876  fourierdlem93  44901  smfpimne2  45542  elprneb  45725  dfatcolem  45949  ichim  46111  ichnfb  46119  prproropf1olem1  46157  prproropf1olem3  46159  rabsubmgmd  46547  2zlidl  46785  lspsslco  47071  isthincd2  47611  fullthinc  47619