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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  syl2anb  599  anabsan  664  eqtr2OLD  2758  pm13.181OLD  3025  rmob  3885  sspsstr  4106  disjne  4455  rexopabb  5529  seex  5639  xpcan2  6177  tron  6388  fcof  6741  fssres  6758  funbrfvb  6947  funopfvb  6948  fvco  6990  fvimacnvi  7054  ffvresb  7124  funressn  7157  funresdfunsn  7187  fvtp2  7197  fvtp2g  7200  fnex  7219  funex  7221  ordsucss  7806  ordsucelsuc  7810  1st2nd  8025  1stconst  8086  2ndconst  8087  frxp  8112  imacosupp  8194  dftpos4  8230  tz7.48lem  8441  nnmsucr  8625  nnmcan  8634  xpmapenlem  9144  imafi  9175  php  9210  php4  9213  phpOLD  9222  isfinite2  9301  fundmfibi  9331  fiinfcl  9496  wofib  9540  r1limg  9766  r1pwcl  9842  cardmin2  9994  zornn0g  10500  mptct  10533  intgru  10809  supsrlem  11106  nzadd  12610  fnn0ind  12661  uztrn2  12841  nnwo  12897  irradd  12957  qbtwnxr  13179  xltnegi  13195  xaddnemnf  13215  xaddnepnf  13216  xaddcom  13219  xnegdi  13227  elioore  13354  uzsubsubfz1  13524  fzo1fzo0n0  13683  elfzonelfzo  13734  modsumfzodifsn  13909  leexp2  14136  faclbnd  14250  faclbnd3  14252  fi1uzind  14458  brfi1uzind  14459  opfi1uzind  14462  swrdccat3b  14690  dvdslelem  16252  divalglem1  16337  dvdsprime  16624  pcgcd  16811  cntri  19196  cntzsgrpcl  19198  efgsrel  19602  xrsdsreclb  20992  znf1o  21107  restuni  22666  stoig  22667  restperf  22688  resstps  22691  pnfnei  22724  mnfnei  22725  cnnei  22786  cmpsublem  22903  comppfsc  23036  tx1stc  23154  xkopt  23159  isfcls  23513  tgioo  24312  opnreen  24347  iscmet3  24810  dyaddisj  25113  limcmpt  25400  degltlem1  25590  ulmdvlem3  25914  lgsdi  26837  noreson  27163  divsclw  27642  cusgrres  28705  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  wwlksnred  29146  eupth2lem3lem4  29484  grpoidinvlem3  29759  ipasslem3  30086  spanuni  30797  5oalem3  30909  5oalem5  30911  mdslmd1lem2  31579  mptctf  31942  xaddeq0  31966  xnn0gt0  31982  ssmxidllem  32589  ssmxidl  32590  ordtconnlem1  32904  esumcvg  33084  ldgenpisyslem1  33161  measdivcst  33222  measdivcstALTV  33223  probun  33418  fnrelpredd  34092  fineqvrep  34095  elmpps  34564  dfon2lem9  34763  funpartfun  34915  cgrxfr  35027  segcon2  35077  brsegle2  35081  seglecgr12im  35082  segletr  35086  nn0prpw  35208  bj-seex  35802  bj-prmoore  35996  fvineqsneu  36292  lindsenlbs  36483  matunitlindflem2  36485  ptrecube  36488  poimirlem28  36516  ftc1anclem5  36565  ftc1anc  36569  exlimddvfi  36990  riccrng1  41096  ricdrng1  41102  nn0addcom  41323  nn0mulcom  41327  mzpclall  41465  4an31  43259  cnrefiisplem  44545  iundjiun  45176  funbrafvb  45864  funopafvb  45865  afvco2  45884  dfatbrafv2b  45953  funbrafv22b  45958  funopafv2b  45959  sprsymrelfolem2  46161  line2xlem  47439  itsclc0xyqsol  47454  f1mo  47519  catprs  47631  setrec2lem2  47739