Theorem sylanb 584

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  syl2anb  600  anabsan  664  eqtr2  2779  pm13.181  3033  rmob  3796  sspsstr  4011  disjne  4351  rexopabb  5385  seex  5487  xpcan2  6006  tron  6192  fssres  6529  funbrfvb  6708  funopfvb  6709  fvco  6750  fvimacnvi  6813  ffvresb  6879  funressn  6912  funresdfunsn  6942  fvtp2  6949  fvtp2g  6952  fnex  6971  funex  6973  ordsucss  7532  ordsucelsuc  7536  1st2nd  7742  1stconst  7800  2ndconst  7801  frxp  7825  imacosupp  7884  dftpos4  7921  tz7.48lem  8087  nnmsucr  8261  nnmcan  8270  xpmapenlem  8706  php  8723  php4  8726  imafi  8743  isfinite2  8809  fundmfibi  8836  fiinfcl  8998  wofib  9042  r1limg  9233  r1pwcl  9309  cardmin2  9461  zornn0g  9965  mptct  9998  intgru  10274  supsrlem  10571  nzadd  12069  fnn0ind  12120  uztrn2  12301  nnwo  12353  irradd  12413  qbtwnxr  12634  xltnegi  12650  xaddnemnf  12670  xaddnepnf  12671  xaddcom  12674  xnegdi  12682  elioore  12809  uzsubsubfz1  12979  fzo1fzo0n0  13137  elfzonelfzo  13188  modsumfzodifsn  13361  leexp2  13585  faclbnd  13700  faclbnd3  13702  fi1uzind  13907  brfi1uzind  13908  opfi1uzind  13911  swrdccat3b  14149  dvdslelem  15710  divalglem1  15795  dvdsprime  16083  pcgcd  16269  cntri  18528  efgsrel  18927  xrsdsreclb  20213  znf1o  20319  restuni  21862  stoig  21863  restperf  21884  resstps  21887  pnfnei  21920  mnfnei  21921  cnnei  21982  cmpsublem  22099  comppfsc  22232  tx1stc  22350  xkopt  22355  isfcls  22709  tgioo  23497  opnreen  23532  iscmet3  23993  dyaddisj  24296  limcmpt  24582  degltlem1  24772  ulmdvlem3  25096  lgsdi  26017  cusgrres  27337  crctcshwlkn0lem4  27698  crctcshwlkn0lem5  27699  wwlksnred  27777  eupth2lem3lem4  28115  grpoidinvlem3  28388  ipasslem3  28715  spanuni  29426  5oalem3  29538  5oalem5  29540  mdslmd1lem2  30208  mptctf  30576  xaddeq0  30600  xnn0gt0  30616  ssmxidllem  31162  ssmxidl  31163  ordtconnlem1  31395  esumcvg  31573  ldgenpisyslem1  31650  measdivcst  31711  measdivcstALTV  31712  probun  31905  fnrelpredd  32590  elmpps  33051  dfon2lem9  33283  noreson  33428  funpartfun  33794  cgrxfr  33906  segcon2  33956  brsegle2  33960  seglecgr12im  33961  segletr  33965  nn0prpw  34061  bj-seex  34646  bj-prmoore  34810  fvineqsneu  35108  lindsenlbs  35332  matunitlindflem2  35334  ptrecube  35337  poimirlem28  35365  ftc1anclem5  35414  ftc1anc  35418  exlimddvfi  35840  mzpclall  40041  4an31  41577  cnrefiisplem  42837  iundjiun  43465  funbrafvb  44080  funopafvb  44081  afvco2  44100  dfatbrafv2b  44169  funbrafv22b  44174  funopafv2b  44175  sprsymrelfolem2  44378  line2xlem  45532  itsclc0xyqsol  45547  setrec2lem2  45615