Theorem sylanb 581

Description: A syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
sylanb.1	⊢ (𝜑 ↔ 𝜓)
sylanb.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylanb	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem sylanb

Step	Hyp	Ref	Expression
1		sylanb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 216	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 580	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  anabsan  665  rmob  3865  sspsstr  4083  disjne  4430  rexopabb  5503  seex  5613  xpcan2  6166  tron  6375  fcof  6728  fssres  6743  funbrfvb  6931  funopfvb  6932  fvco  6976  fvimacnvi  7041  ffvresb  7114  funressn  7148  funresdfunsn  7180  fvtp2  7187  fvtp2g  7190  fnex  7208  funex  7210  ordsucss  7810  ordsucelsuc  7814  1st2nd  8036  1stconst  8097  2ndconst  8098  frxp  8123  imacosupp  8206  dftpos4  8242  tz7.48lem  8453  nnmsucr  8635  nnmcan  8644  xpmapenlem  9156  php  9219  php4  9222  phpOLD  9229  isfinite2  9304  imafiOLD  9324  fundmfibi  9346  fiinfcl  9513  wofib  9557  r1limg  9783  r1pwcl  9859  cardmin2  10011  zornn0g  10517  mptct  10550  intgru  10826  supsrlem  11123  nzadd  12638  fnn0ind  12690  uztrn2  12869  nnwo  12927  irradd  12987  qbtwnxr  13214  xltnegi  13230  xaddnemnf  13250  xaddnepnf  13251  xaddcom  13254  xnegdi  13262  elioore  13390  uzsubsubfz1  13562  fzo1fzo0n0  13729  elfzonelfzo  13783  modsumfzodifsn  13960  leexp2  14187  faclbnd  14306  faclbnd3  14308  fi1uzind  14523  brfi1uzind  14524  opfi1uzind  14527  swrdccat3b  14756  dvdslelem  16326  divalglem1  16411  dvdsprime  16704  pcgcd  16896  cntri  19313  cntzsgrpcl  19315  efgsrel  19713  xrsdsreclb  21379  znf1o  21510  restuni  23098  stoig  23099  restperf  23120  resstps  23123  pnfnei  23156  mnfnei  23157  cnnei  23218  cmpsublem  23335  comppfsc  23468  tx1stc  23586  xkopt  23591  isfcls  23945  tgioo  24733  opnreen  24769  iscmet3  25243  dyaddisj  25547  limcmpt  25834  degltlem1  26027  ulmdvlem3  26361  lgsdi  27295  noreson  27622  divsclw  28137  cusgrres  29374  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  wwlksnred  29820  eupth2lem3lem4  30158  grpoidinvlem3  30433  ipasslem3  30760  spanuni  31471  5oalem3  31583  5oalem5  31585  mdslmd1lem2  32253  mptctf  32641  xaddeq0  32676  xnn0gt0  32692  ssdifidllem  33417  ssmxidllem  33434  ssmxidl  33435  ordtconnlem1  33901  esumcvg  34063  ldgenpisyslem1  34140  measdivcst  34201  measdivcstALTV  34202  probun  34397  fnrelpredd  35066  fineqvrep  35072  elmpps  35541  dfon2lem9  35755  funpartfun  35907  cgrxfr  36019  segcon2  36069  brsegle2  36073  seglecgr12im  36074  segletr  36078  nn0prpw  36287  bj-seex  36886  bj-prmoore  37079  fvineqsneu  37375  lindsenlbs  37585  matunitlindflem2  37587  ptrecube  37590  poimirlem28  37618  ftc1anclem5  37667  ftc1anc  37671  exlimddvfi  38092  imadomfi  41961  readvrec  42352  nn0addcom  42440  nn0mulcom  42444  riccrng1  42491  ricdrng1  42498  mzpclall  42697  4an31  44471  cnrefiisplem  45806  iundjiun  46437  funbrafvb  47133  funopafvb  47134  afvco2  47153  dfatbrafv2b  47222  funbrafv22b  47227  funopafv2b  47228  sprsymrelfolem2  47455  uhgrimgrlim  47947  line2xlem  48681  itsclc0xyqsol  48696  f1mo  48779  catprs  48934  setrec2lem2  49506