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 215	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 580	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  anabsan  663  eqtr2OLD  2757  pm13.181OLD  3024  rmob  3883  sspsstr  4104  disjne  4453  rexopabb  5527  seex  5637  xpcan2  6173  tron  6384  fcof  6737  fssres  6754  funbrfvb  6943  funopfvb  6944  fvco  6986  fvimacnvi  7050  ffvresb  7120  funressn  7153  funresdfunsn  7183  fvtp2  7193  fvtp2g  7196  fnex  7215  funex  7217  ordsucss  7802  ordsucelsuc  7806  1st2nd  8021  1stconst  8082  2ndconst  8083  frxp  8108  imacosupp  8190  dftpos4  8226  tz7.48lem  8437  nnmsucr  8621  nnmcan  8630  xpmapenlem  9140  imafi  9171  php  9206  php4  9209  phpOLD  9218  isfinite2  9297  fundmfibi  9327  fiinfcl  9492  wofib  9536  r1limg  9762  r1pwcl  9838  cardmin2  9990  zornn0g  10496  mptct  10529  intgru  10805  supsrlem  11102  nzadd  12606  fnn0ind  12657  uztrn2  12837  nnwo  12893  irradd  12953  qbtwnxr  13175  xltnegi  13191  xaddnemnf  13211  xaddnepnf  13212  xaddcom  13215  xnegdi  13223  elioore  13350  uzsubsubfz1  13520  fzo1fzo0n0  13679  elfzonelfzo  13730  modsumfzodifsn  13905  leexp2  14132  faclbnd  14246  faclbnd3  14248  fi1uzind  14454  brfi1uzind  14455  opfi1uzind  14458  swrdccat3b  14686  dvdslelem  16248  divalglem1  16333  dvdsprime  16620  pcgcd  16807  cntri  19190  cntzsgrpcl  19192  efgsrel  19596  xrsdsreclb  20984  znf1o  21098  restuni  22657  stoig  22658  restperf  22679  resstps  22682  pnfnei  22715  mnfnei  22716  cnnei  22777  cmpsublem  22894  comppfsc  23027  tx1stc  23145  xkopt  23150  isfcls  23504  tgioo  24303  opnreen  24338  iscmet3  24801  dyaddisj  25104  limcmpt  25391  degltlem1  25581  ulmdvlem3  25905  lgsdi  26826  noreson  27152  divsclw  27631  cusgrres  28694  crctcshwlkn0lem4  29056  crctcshwlkn0lem5  29057  wwlksnred  29135  eupth2lem3lem4  29473  grpoidinvlem3  29746  ipasslem3  30073  spanuni  30784  5oalem3  30896  5oalem5  30898  mdslmd1lem2  31566  mptctf  31929  xaddeq0  31953  xnn0gt0  31969  ssmxidllem  32577  ssmxidl  32578  ordtconnlem1  32892  esumcvg  33072  ldgenpisyslem1  33149  measdivcst  33210  measdivcstALTV  33211  probun  33406  fnrelpredd  34080  fineqvrep  34083  elmpps  34552  dfon2lem9  34751  funpartfun  34903  cgrxfr  35015  segcon2  35065  brsegle2  35069  seglecgr12im  35070  segletr  35074  nn0prpw  35196  bj-seex  35790  bj-prmoore  35984  fvineqsneu  36280  lindsenlbs  36471  matunitlindflem2  36473  ptrecube  36476  poimirlem28  36504  ftc1anclem5  36553  ftc1anc  36557  exlimddvfi  36978  riccrng1  41093  ricdrng1  41099  nn0addcom  41319  nn0mulcom  41323  mzpclall  41450  4an31  43244  cnrefiisplem  44531  iundjiun  45162  funbrafvb  45850  funopafvb  45851  afvco2  45870  dfatbrafv2b  45939  funbrafv22b  45944  funopafv2b  45945  sprsymrelfolem2  46147  line2xlem  47392  itsclc0xyqsol  47407  f1mo  47472  catprs  47584  setrec2lem2  47692