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 217	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 580	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  syl2anb  597  anabsan  661  eqtr2  2819  pm13.181  3069  rmob  3808  sspsstr  4009  disjne  4324  rexopabb  5312  seex  5413  xpcan2  5917  tron  6096  fssres  6419  funbrfvb  6595  funopfvb  6596  fvco  6633  fvimacnvi  6694  ffvresb  6758  funressn  6791  funresdfunsn  6825  fvtp2  6832  fvtp2g  6835  fnex  6853  funex  6855  ordsucss  7396  ordsucelsuc  7400  1st2nd  7601  1stconst  7658  2ndconst  7659  frxp  7680  imacosupp  7732  dftpos4  7769  tz7.48lem  7935  nnmsucr  8108  nnmcan  8117  xpmapenlem  8538  php  8555  php4  8558  isfinite2  8629  fundmfibi  8656  fiinfcl  8818  wofib  8862  r1limg  9053  r1pwcl  9129  cardmin2  9280  zornn0g  9780  mptct  9813  intgru  10089  supsrlem  10386  nzadd  11884  fnn0ind  11935  uztrn2  12115  nnwo  12166  irradd  12226  qbtwnxr  12447  xltnegi  12463  xaddnemnf  12483  xaddnepnf  12484  xaddcom  12487  xnegdi  12495  elioore  12622  uzsubsubfz1  12784  fzo1fzo0n0  12942  elfzonelfzo  12993  modsumfzodifsn  13166  leexp2  13389  faclbnd  13504  faclbnd3  13506  fi1uzind  13705  brfi1uzind  13706  opfi1uzind  13709  swrdccat3b  13942  dvdslelem  15496  divalglem1  15582  dvdsprime  15864  pcgcd  16047  cntri  18206  efgsrel  18591  xrsdsreclb  20278  znf1o  20384  restuni  21458  stoig  21459  restperf  21480  resstps  21483  pnfnei  21516  mnfnei  21517  cnnei  21578  cmpsublem  21695  comppfsc  21828  tx1stc  21946  xkopt  21951  isfcls  22305  tgioo  23091  opnreen  23126  iscmet3  23583  dyaddisj  23884  limcmpt  24168  degltlem1  24353  ulmdvlem3  24677  lgsdi  25596  cusgrres  26917  crctcshwlkn0lem4  27277  crctcshwlkn0lem5  27278  wwlksnred  27356  eupth2lem3lem4  27696  grpoidinvlem3  27970  ipasslem3  28297  spanuni  29008  5oalem3  29120  5oalem5  29122  mdslmd1lem2  29790  mptctf  30137  xaddeq0  30161  xnn0gt0  30178  ordtconnlem1  30780  esumcvg  30958  ldgenpisyslem1  31035  measres  31094  measdivcst  31096  measdivcstALTV  31097  probun  31290  elmpps  32430  dfon2lem9  32646  noreson  32778  funpartfun  33015  cgrxfr  33127  segcon2  33177  brsegle2  33181  seglecgr12im  33182  segletr  33186  nn0prpw  33282  bj-seex  33818  fvineqsneu  34244  lindsenlbs  34439  matunitlindflem2  34441  ptrecube  34444  poimirlem28  34472  ftc1anclem5  34523  ftc1anc  34527  exlimddvfi  34953  mzpclall  38830  4an31  40392  cnrefiisplem  41673  iundjiun  42306  funbrafvb  42893  funopafvb  42894  afvco2  42913  dfatbrafv2b  42982  funbrafv22b  42987  funopafv2b  42988  sprsymrelfolem2  43159  line2xlem  44243  itsclc0xyqsol  44258  setrec2lem2  44299