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  3853  sspsstr  4071  disjne  4418  rexopabb  5488  seex  5597  xpcan2  6150  tron  6355  fcof  6711  fssres  6726  funbrfvb  6914  funopfvb  6915  fvco  6959  fvimacnvi  7024  ffvresb  7097  funressn  7131  funresdfunsn  7163  fvtp2  7170  fvtp2g  7173  fnex  7191  funex  7193  ordsucss  7793  ordsucelsuc  7797  1st2nd  8018  1stconst  8079  2ndconst  8080  frxp  8105  imacosupp  8188  dftpos4  8224  tz7.48lem  8409  nnmsucr  8589  nnmcan  8598  xpmapenlem  9108  php  9171  php4  9174  isfinite2  9245  imafiOLD  9265  fundmfibi  9287  fiinfcl  9454  wofib  9498  r1limg  9724  r1pwcl  9800  cardmin2  9952  zornn0g  10458  mptct  10491  intgru  10767  supsrlem  11064  nzadd  12581  fnn0ind  12633  uztrn2  12812  nnwo  12872  irradd  12932  qbtwnxr  13160  xltnegi  13176  xaddnemnf  13196  xaddnepnf  13197  xaddcom  13200  xnegdi  13208  elioore  13336  uzsubsubfz1  13508  fzo1fzo0n0  13676  elfzonelfzo  13730  modsumfzodifsn  13909  leexp2  14136  faclbnd  14255  faclbnd3  14257  fi1uzind  14472  brfi1uzind  14473  opfi1uzind  14476  swrdccat3b  14705  dvdslelem  16279  divalglem1  16364  dvdsprime  16657  pcgcd  16849  cntri  19264  cntzsgrpcl  19266  efgsrel  19664  xrsdsreclb  21330  znf1o  21461  restuni  23049  stoig  23050  restperf  23071  resstps  23074  pnfnei  23107  mnfnei  23108  cnnei  23169  cmpsublem  23286  comppfsc  23419  tx1stc  23537  xkopt  23542  isfcls  23896  tgioo  24684  opnreen  24720  iscmet3  25193  dyaddisj  25497  limcmpt  25784  degltlem1  25977  ulmdvlem3  26311  lgsdi  27245  noreson  27572  divsclw  28098  cusgrres  29376  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  wwlksnred  29822  eupth2lem3lem4  30160  grpoidinvlem3  30435  ipasslem3  30762  spanuni  31473  5oalem3  31585  5oalem5  31587  mdslmd1lem2  32255  mptctf  32641  xaddeq0  32676  xnn0gt0  32692  ssdifidllem  33427  ssmxidllem  33444  ssmxidl  33445  ordtconnlem1  33914  esumcvg  34076  ldgenpisyslem1  34153  measdivcst  34214  measdivcstALTV  34215  probun  34410  fnrelpredd  35079  fineqvrep  35085  elmpps  35560  dfon2lem9  35779  funpartfun  35931  cgrxfr  36043  segcon2  36093  brsegle2  36097  seglecgr12im  36098  segletr  36102  nn0prpw  36311  bj-seex  36910  bj-prmoore  37103  fvineqsneu  37399  lindsenlbs  37609  matunitlindflem2  37611  ptrecube  37614  poimirlem28  37642  ftc1anclem5  37691  ftc1anc  37695  exlimddvfi  38116  imadomfi  41990  readvrec  42350  nn0addcom  42450  nn0mulcom  42454  riccrng1  42509  ricdrng1  42516  mzpclall  42715  4an31  44488  cnrefiisplem  45827  iundjiun  46458  funbrafvb  47157  funopafvb  47158  afvco2  47177  dfatbrafv2b  47246  funbrafv22b  47251  funopafv2b  47252  sprsymrelfolem2  47494  uhgrimgrlim  47986  line2xlem  48742  itsclc0xyqsol  48757  f1mo  48841  catprs  49000  setrec2lem2  49683