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  3842  sspsstr  4062  disjne  4409  rexopabb  5486  seex  5593  xpcan2  6145  tron  6350  fcof  6695  fssres  6710  funbrfvb  6897  funopfvb  6898  fvco  6942  fvimacnvi  7008  ffvresb  7082  funressn  7116  funresdfunsn  7147  fvtp2  7154  fvtp2g  7157  fnex  7175  funex  7177  ordsucss  7772  ordsucelsuc  7776  1st2nd  7995  1stconst  8054  2ndconst  8055  frxp  8080  imacosupp  8163  dftpos4  8199  tz7.48lem  8384  nnmsucr  8565  nnmcan  8574  xpmapenlem  9086  php  9145  php4  9148  isfinite2  9212  imafiOLD  9230  fundmfibi  9250  fiinfcl  9420  wofib  9464  r1limg  9697  r1pwcl  9773  cardmin2  9925  zornn0g  10429  mptct  10462  intgru  10739  supsrlem  11036  nzadd  12553  fnn0ind  12605  uztrn2  12784  nnwo  12840  irradd  12900  qbtwnxr  13129  xltnegi  13145  xaddnemnf  13165  xaddnepnf  13166  xaddcom  13169  xnegdi  13177  elioore  13305  uzsubsubfz1  13477  fzo1fzo0n0  13645  elfzonelfzo  13699  modsumfzodifsn  13881  leexp2  14108  faclbnd  14227  faclbnd3  14229  fi1uzind  14444  brfi1uzind  14445  opfi1uzind  14448  swrdccat3b  14677  dvdslelem  16250  divalglem1  16335  dvdsprime  16628  pcgcd  16820  cntri  19278  cntzsgrpcl  19280  efgsrel  19680  xrsdsreclb  21385  znf1o  21523  restuni  23123  stoig  23124  restperf  23145  resstps  23148  pnfnei  23181  mnfnei  23182  cnnei  23243  cmpsublem  23360  comppfsc  23493  tx1stc  23611  xkopt  23616  isfcls  23970  tgioo  24757  opnreen  24793  iscmet3  25266  dyaddisj  25570  limcmpt  25857  degltlem1  26050  ulmdvlem3  26384  lgsdi  27318  noreson  27645  divsclw  28208  cusgrres  29540  crctcshwlkn0lem4  29904  crctcshwlkn0lem5  29905  wwlksnred  29983  eupth2lem3lem4  30324  grpoidinvlem3  30600  ipasslem3  30927  spanuni  31638  5oalem3  31750  5oalem5  31752  mdslmd1lem2  32420  rnressnsn  32773  mptctf  32812  xaddeq0  32850  xnn0gt0  32866  ssdifidllem  33555  ssmxidllem  33572  ssmxidl  33573  ordtconnlem1  34108  esumcvg  34270  ldgenpisyslem1  34347  measdivcst  34408  measdivcstALTV  34409  probun  34603  fnrelpredd  35274  elwf  35280  r1omhf  35289  fineqvrep  35298  elmpps  35795  dfon2lem9  36011  funpartfun  36165  cgrxfr  36277  segcon2  36327  brsegle2  36331  seglecgr12im  36332  segletr  36336  nn0prpw  36545  bj-seex  37197  bj-axreprepsep  37350  bj-prmoore  37395  fvineqsneu  37693  lindsenlbs  37895  matunitlindflem2  37897  ptrecube  37900  poimirlem28  37928  ftc1anclem5  37977  ftc1anc  37981  exlimddvfi  38402  imadomfi  42401  readvrec  42761  nn0addcom  42861  nn0mulcom  42865  riccrng1  42920  ricdrng1  42927  mzpclall  43113  4an31  44883  cnrefiisplem  46216  iundjiun  46847  funbrafvb  47545  funopafvb  47546  afvco2  47565  dfatbrafv2b  47634  funbrafv22b  47639  funopafv2b  47640  sprsymrelfolem2  47882  uhgrimgrlim  48376  line2xlem  49142  itsclc0xyqsol  49157  f1mo  49241  catprs  49399  setrec2lem2  50082