Theorem sylanb 582

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 581	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  599  anabsan  666  rmob  3829  sspsstr  4049  disjne  4396  rexopabb  5476  seex  5583  xpcan2  6135  tron  6340  fcof  6685  fssres  6700  funbrfvb  6887  funopfvb  6888  fvco  6932  fvimacnvi  6998  ffvresb  7072  funressn  7106  funresdfunsn  7137  fvtp2  7144  fvtp2g  7147  fnex  7165  funex  7167  ordsucss  7762  ordsucelsuc  7766  1st2nd  7985  1stconst  8043  2ndconst  8044  frxp  8069  imacosupp  8152  dftpos4  8188  tz7.48lem  8373  nnmsucr  8554  nnmcan  8563  xpmapenlem  9075  php  9134  php4  9137  isfinite2  9201  imafiOLD  9219  fundmfibi  9239  fiinfcl  9409  wofib  9453  r1limg  9686  r1pwcl  9762  cardmin2  9914  zornn0g  10418  mptct  10451  intgru  10728  supsrlem  11025  nzadd  12566  fnn0ind  12619  uztrn2  12798  nnwo  12854  irradd  12914  qbtwnxr  13143  xltnegi  13159  xaddnemnf  13179  xaddnepnf  13180  xaddcom  13183  xnegdi  13191  elioore  13319  uzsubsubfz1  13492  fzo1fzo0n0  13661  elfzonelfzo  13715  modsumfzodifsn  13897  leexp2  14124  faclbnd  14243  faclbnd3  14245  fi1uzind  14460  brfi1uzind  14461  opfi1uzind  14464  swrdccat3b  14693  dvdslelem  16269  divalglem1  16354  dvdsprime  16647  pcgcd  16840  cntri  19298  cntzsgrpcl  19300  efgsrel  19700  xrsdsreclb  21403  znf1o  21541  restuni  23137  stoig  23138  restperf  23159  resstps  23162  pnfnei  23195  mnfnei  23196  cnnei  23257  cmpsublem  23374  comppfsc  23507  tx1stc  23625  xkopt  23630  isfcls  23984  tgioo  24771  opnreen  24807  iscmet3  25270  dyaddisj  25573  limcmpt  25860  degltlem1  26047  ulmdvlem3  26380  lgsdi  27311  noreson  27638  divsclw  28201  cusgrres  29532  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  wwlksnred  29975  eupth2lem3lem4  30316  grpoidinvlem3  30592  ipasslem3  30919  spanuni  31630  5oalem3  31742  5oalem5  31744  mdslmd1lem2  32412  rnressnsn  32765  mptctf  32804  xaddeq0  32841  xnn0gt0  32857  ssdifidllem  33531  ssmxidllem  33548  ssmxidl  33549  ordtconnlem1  34084  esumcvg  34246  ldgenpisyslem1  34323  measdivcst  34384  measdivcstALTV  34385  probun  34579  fnrelpredd  35250  elwf  35256  r1omhf  35265  fineqvrep  35274  elmpps  35771  dfon2lem9  35987  funpartfun  36141  cgrxfr  36253  segcon2  36303  brsegle2  36307  seglecgr12im  36308  segletr  36312  nn0prpw  36521  bj-seex  37245  bj-axreprepsep  37398  bj-prmoore  37443  fvineqsneu  37741  lindsenlbs  37950  matunitlindflem2  37952  ptrecube  37955  poimirlem28  37983  ftc1anclem5  38032  ftc1anc  38036  exlimddvfi  38457  imadomfi  42455  readvrec  42808  nn0addcom  42921  nn0mulcom  42925  riccrng1  42980  ricdrng1  42987  mzpclall  43173  4an31  44943  cnrefiisplem  46275  iundjiun  46906  funbrafvb  47616  funopafvb  47617  afvco2  47636  dfatbrafv2b  47705  funbrafv22b  47710  funopafv2b  47711  sprsymrelfolem2  47965  uhgrimgrlim  48475  line2xlem  49241  itsclc0xyqsol  49256  f1mo  49340  catprs  49498  setrec2lem2  50181